Título:
|
Proving termination of imperative programs using Max-SMT
|
Autor/a:
|
Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
|
Otros autores:
|
Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics; Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació |
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. |
Abstract:
|
Peer Reviewed |
Materia(s):
|
-Àrees temàtiques de la UPC::Informàtica::Programació -Max-SMT -Program correctness -Termination analysis -Invariant synthesis -Programació lògica amb restriccions |
Derechos:
|
|
Tipo de documento:
|
Artículo - Borrador Objeto de conferencia |
Compartir:
|
|