Sciweavers

ISSTA
2010
ACM

Analysis of invariants for efficient bounded verification

13 years 5 months ago
Analysis of invariants for efficient bounded verification
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 error 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 that 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 in the experiments we have carried out to an improvement on the efficiency of the anal...
Juan P. Galeotti, Nicolás Rosner, Carlos L&
Added 13 Oct 2010
Updated 13 Oct 2010
Type Conference
Year 2010
Where ISSTA
Authors Juan P. Galeotti, Nicolás Rosner, Carlos López Pombo, Marcelo F. Frias
Comments (0)