Carregant...
Carregant...

Vés al contingut (premeu Retorn)

Proving termination of imperative programs using Max-SMT

Autor
Larraz, D.; Oliveras, A.; Rodriguez, E.; Rubio, A.
Tipus d'activitat
Presentació treball a congrés
Nom de l'edició
Formal Methods in Computer-Aided Design
Any de l'edició
2013
Data de presentació
2013-10-23
Llibre d'actes
FMCAD 2013 : Formal Methods in Computer–Aided Design : Portland, OR, USA, 20–23 October 2013
Pàgina inicial
218
Pàgina final
225
Projecte finançador
Sweetlogics-UPC
Repositori
http://hdl.handle.net/2117/20895 Obrir en finestra nova
URL
http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/proceedings.shtml Obrir en finestra nova
Resum
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 ...
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.
Paraules clau
Invariant synthesis, Max-SMT, Program correctness, Termination analysis
Grup de recerca
LOGPROG - Lògica i Programació

Participants

Arxius