TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds
by
Juan Pablo Galeotti, Nicolas Rosner, Carlos G. Lopez Pombo, Marcelo F. Frias
IEEE Transactions on Software Engineering, Pages 1283-1307, Volume 39, Number 9, September 2013.
Digital Library via DOI: 10.1109/TSE.2013.15 - Local copy: Download as PDF file.
See also
More information is available at http://www.dc.uba.ar/taco.
Abstract
SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the failure is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this article we present TACO, a prototype tool which implements a novel, general and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument code analysis with a symmetry-breaking predicate which, on one hand, reduces the size of the search space by ignoring certain classes of isomorphic models, and on the other hand, allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading to an improvement of the efficiency of the analysis of orders of magnitude, compared to the non-instrumented SAT-based analysis. We show that, in some cases, our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking or SMT-solving.
Keywords
- Static analysis
- SAT-based code analysis
- Alloy
- KodKod
- DynAlloy
BibTeX Entry
@article{galeotti-tse-2013,
title = "TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds",
author = "Juan Pablo Galeotti and Nicolas Rosner and Carlos G. Lopez Pombo and Marcelo F. Frias",
year = "2013",
month = sep,
journal = "IEEE Transactions on Software Engineering",
number = "9",
pages = "1283--1307",
volume = "39",
doi = "10.1109/TSE.2013.15",
}