If you do not see this message displayed properly, please click here


The Faculty of Informatics is pleased to announce a seminar given by Alexey Bakhirkin



Towards finding non-terminating behaviours in programs
Speaker: Alexey Bakhirkin
University of Leicester, UK
Date: Thursday, May 12, 2016
Place: USI Lugano Campus, room SI-008, Informatics building (Via G. Buffi 13)
Time: 10:30



We present our take on a problem of finding a recurrent set of an imperative program. A recurrent set is a set of states that, once reached, cannot or may not be escaped by an execution (there exist multiple definitions). A straightforward application of a recurrent set is to show the existence of non-terminating executions in the program, for that it needs to be complemented by a proof of reachablility from some initial state. And there are also other analyses that have finding a recurrent set as a sub-problem. We developed two algorithms for finding recurrent sets in programs. One is based on symbolic execution and is suitable for non-numeric (e.g., heap-manipulating) programs.
Another is based on backwards analysis via abstract interpretation and is more geared towards numeric programs.



Alexey is a PhD student in the University of Leicester (UK), where his research is into abstract interpretation and its application to termination and non-termination analyses. Before that, he was studying computing in Bauman University in Moscow.


Host: Prof. Natasha Sharygina


Faculty of Informatics

Faculty of Informatics
Università della Svizzera italiana
Via Giuseppe Buffi 13
CH-6904 Lugano
Tel.: +41 (0)58 666 46 90
Fax: +41 (0)58 666 45 36
Email: decanato.inf@usi.ch
Web: www.inf.usi.ch
Twitter: @USI_INF


Segui USI@EXPO2015 su Twitter Segui USI@EXPO2015 su Facebook Segui USI@EXPO2015 su Linkedin Segui USI@EXPO2015 su YouTube