+********************************************************************** * * *Einladung * * * *Informatik-Oberseminar * * * +**********************************************************************
Zeit: Donnerstag, 12. Okt. 2023, 09:00 Uhr Ort: Informatikzentrum der RWTH Aachen University, Gebäude E3, 2. Etage, Raum 9222 Referent: Jera Hensel, M.Sc. Lehr- und Forschungsgebiet Informatik 2 Thema: Automated Termination Analysis of C Programs Abstract:
The termination behavior of a program is a crucial property when reasoning about its correctness and safety. Non-termination and also undesired termination can lead to serious consequences such as system crashes and security vulnerabilities. Therefore, we are interested in techniques to (dis)prove termination of programs to make software systems more secure and reliable. Analyzing the termination behavior of C programs is especially challenging since C combines concepts of higher programming languages with pointers and explicit memory management.
In this talk, we summarize our improvements of a termination analysis approach that is especially powerful for C programs with memory allocation and explicit pointer arithmetic, but which was limited to rather small non-recursive programs without recursive data structures, where all integers were interpreted as unbounded (mathematical) integers. This approach uses symbolic execution with abstraction to convert the analyzed program to an integer transition system (ITS) with the property that termination of this ITS implies termination of the C program. Thus, after this transformation, existing techniques for ITSs can be applied to prove termination of the program. We lift the above mentioned restrictions by new techniques that only require adaptions of the symbolic execution rules and the abstraction methods, but use the same transformation to ITSs as before. Moreover, we briefly show how this approach is modified to prove non-termination. We implemented all extensions in our tool AProVE and evaluate them in comparison with other leading termination tools.
Es laden ein: die Dozentinnen und Dozenten der Informatik --
Elke Ohlenforst Softwaremodellierung und Verifikation Lehrstuhl Informatik 2, RWTH Aachen Ahornstr. 55, D-52074 Aachen/Germany Tel.: +49 (0)241 80-21201 email:ohlenforst@informatik.rwth-aachen.de https://moves.rwth-aachen.de/