Para acceder a los documentos con el texto completo, por favor, siga el siguiente enlace: http://hdl.handle.net/2117/102254

Speeding up the constraint-based method in difference logic
Candeago, L.; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació
"The final publication is available at http://link.springer.com/chapter/10.1007%2F978-3-319-40970-2_18"
Over the years the constraint-based method has been successfully applied to a wide range of problems in program analysis, from invariant generation to termination and non-termination proving. Quite often the semantics of the program under study as well as the properties to be generated belong to difference logic, i.e., the fragment of linear arithmetic where atoms are inequalities of the form u v = k. However, so far constraint-based techniques have not exploited this fact: in general, Farkas’ Lemma is used to produce the constraints over template unknowns, which leads to non-linear SMT problems. Based on classical results of graph theory, in this paper we propose new encodings for generating these constraints when program semantics and templates belong to difference logic. Thanks to this approach, instead of a heavyweight non-linear arithmetic solver, a much cheaper SMT solver for difference logic or linear integer arithmetic can be employed for solving the resulting constraints. We present encouraging experimental results that show the high impact of the proposed techniques on the performance of the VeryMax verification system
Peer Reviewed
Àrees temàtiques de la UPC::Informàtica::Intel·ligència artificial
Boolean satisfiability problem
Formal logic
Graph theory
Reconfigurable hardware
Semantics
Constraint based method
Integer arithmetic
Invariant generations
Linear arithmetic
Non terminations
Program analysis
Program semantics
Verification systems
Computer circuits
Problema de satisfacibilitat booleana
info:eu-repo/semantics/submittedVersion
info:eu-repo/semantics/conferenceObject
         

Mostrar el registro completo del ítem

Documentos relacionados

Otros documentos del mismo autor/a

Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Larraz Hurtado, Daniel; Nimkar, Kaustubh; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Asín Acha, Roberto Javier; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric