Speeding up the constraint-based method in difference logic
| Autor: | Enric Rodríguez-Carbonell, Daniel Larraz, Albert Oliveras, Lorenzo Candeago, Albert Rubio |
|---|---|
| Přispěvatelé: | Universitat Politècnica de Catalunya. Departament de Ciències de la Computació, Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació |
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Invariant generations
Non terminations Linear arithmetic Verification systems Of the form 02 engineering and technology Integer arithmetic Formal logic Program analysis Satisfiability modulo theories Lemma (logic) Quantifier elimination 0202 electrical engineering electronic engineering information engineering Mathematics Problema de satisfacibilitat booleana 020207 software engineering Graph theory Solver Computer circuits Reconfigurable computing Reconfigurable hardware Semantics 020201 artificial intelligence & image processing Informàtica::Intel·ligència artificial [Àrees temàtiques de la UPC] Boolean satisfiability problem Algorithm Program semantics Constraint based method |
| Zdroj: | UPCommons. Portal del coneixement obert de la UPC Universitat Politècnica de Catalunya (UPC) Theory and Applications of Satisfiability Testing – SAT 2016 ISBN: 9783319409696 SAT Recercat. Dipósit de la Recerca de Catalunya instname |
| Popis: | "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 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|