Proving termination of imperative programs using Max-SMT
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/20895
Tipus de documentText en actes de congrés
Data publicació2013
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 can be exploited in constraint-based program termination proving. Thanks to expressing the generation of a ranking function as a Max-SMT optimization problem where constraints are assigned different weights, quasi-ranking functions --functions that almost satisfy all conditions for ensuring well-foundedness-- are produced in a lack of ranking functions. By means of trace partitioning, this allows our method to progress in the termination analysis where other approaches would get stuck. Moreover, Max-SMT makes it easy to combine the process of building the termination argument with the usually necessary task of generating supporting invariants. The method has been implemented in a prototype that has successfully been tested on a wide set of programs.
CitacióLarraz, D. [et al.]. Proving termination of imperative programs using Max-SMT. A: FMCAD 2013 Formal Methods in Computer-Aided Design. "International Conference on Formal Methods in Computer-Aided Design". Portland, Oregon: 2013, p. 218-225.
ISBN978-0-9835678-3-7/13
Versió de l'editorhttp://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/proceedings.shtml
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
Larraz et al.pdf | 170,9Kb | Visualitza/Obre |