Analysis of Invariants for Efficient Bounded Verification
Speaker: Juan Pablo Galeotti , University of Buenos Aires
Date: March 15 2011
Time: 2:30PM to 3:30PM
Location: 32-G882 (Hewlett Room)
Host: Daniel Jackson, CSAIL, MIT
Contact: Eunsuk Kang, eskang@mit.edu
SAT-based bounded verification of annotated code consists of translating the code together and its specification to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation to the specification is found, an execution trace exposing the error is exhibited.
In this talk we will present TACO (Translation of Annotated COde). TACO translates annotated Java programs into an Alloy model using Dijkstra's weakest precondition. TACO includes a novel, general and fully automated technique for the SAT-based analysis of sequential programs dealing with complex linked data structures.
The intermediate Alloy representation is instrumented with a symmetry-breaking predicate allowing 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 a speedup on the analysis of orders of magnitude compared to the non-instrumented SAT-based analysis.
This novel technique allowed TACO to successfully revealed an error in a benchmark program that had supposedly been subjected to rigorous analysis in previous experiments with other tools.
Bio:
Juan Pablo is an assistant researcher from CONICET at the School of Natural and Exact Sciences of the University of Buenos Aires. He has a Doctorate in Computer Science in Software Engineering. His research interests are mainly focused towards the software testing and verification. In particular he's working (or have recently worked) in bounded contract verification, program analysis, programming languages design, and model checking. He is a member of the Relational Formal Methods headed by Dr. Marcelo Frias and of the local Software Engineering Research Area.
See other events that are part of
See other events happening in March 2011
