Towards finding non-terminating behaviours in programs
Staff - Faculty of Informatics
Start date: 12 May 2016
End date: 13 May 2016
|
|||||||||||
|
|
|||||||||||
| Abstract: | |||||||||||
|
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. |
|||||||||||
|
|
|||||||||||
| Biography: | |||||||||||
|
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. |
|||||||||||
|
|
|||||||||||
|
|||||||||||
