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...

• Type: Conference
• Year: 2010
• Where: ISSTA
• Authors: Juan P. Galeotti, Nicolás Rosner, Carlos López Pombo, Marcelo F. Frias
• Keywords: ISSTA 2010, Propositional Formulas, SAT-based Analysis, SAT-based Bounded Verification, Software Engineering