Proving non-termination using max-SMT
Visualitza/Obre
10.1007/978-3-319-08867-9_52
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/24334
Tipus de documentText en actes de congrés
Data publicació2014
EditorSpringer
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Abstract
We show how Max-SMT-based invariant generation can be exploited for proving non-termination of programs. The construction of the proof of non-termination is guided by the generation of quasi-invariants - properties such that if they hold at a location during execution once, then they will continue to hold at that location from then onwards. The check that quasi-invariants can indeed be reached is then performed separately. Our technique considers strongly connected subgraphs of a program's control flow graph for analysis and thus produces more generic witnesses of non-termination than existing methods. Moreover, it can handle programs with unbounded non-determinism and is more likely to converge than previous approaches.
CitacióLarraz, D. [et al.]. Proving non-termination using max-SMT. A: International Conference on Computer Aided Verification. "Computer Aided Verification : 26th International Conference CAV 2014 : held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014 : Proceedings". Vienna: Springer, 2014, p. 779-796.
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
cav14.pdf | 165,2Kb | Visualitza/Obre |