[PRL] [MIT Thesis Defense] Finding Bugs in Software with a SAT Solver

Mitchell Wand wand at ccs.neu.edu
Sun Nov 2 21:47:55 EST 2003


Finding Bugs in Software with a SAT Solver
Speaker: Mandana Vaziri
Speaker Affiliation: MIT
Host: J. Guttag, D. Jackson (supervisor), M. Rinard
Host Affiliation: MIT

Date: 11-5-2003
Time: 10:00 AM - 12:00 PM
Refreshments: 9:45 AM
Location: NE43-518

We present a static technique for finding bugs in object-oriented
procedures. It is capable of checking complex user-defined structural
properties -- that is, of the configuration of objects on the heap --
and generates counterexample traces with no false alarms. It is
modular, requires no user-provided abstractions, and is fully
automatic. 

It is based on the Alloy modelling language and analyzer. The method
relies on a three-step translation: from code to a formula in Alloy,
which is a first-order relational logic, then to a propositional
formula, and finally to conjunctive normal form.  An off-the-shelf SAT
solver is then used to find a solution that constitutes a
counterexample. 

Modularity comes at the price of intermediate specifications. To
minimize such annotations, the analysis contains a suite of
optimizations that allow checking larger procedures with fewer
annotations. The optimizations are based on a special treatment of
relations that are known to be functional, and target all steps of the
translation to CNF. Their effect is demonstrated with a prototype tool
that can handle a subset of Java, by analyzing real code. 

Thesis Committee:
John Guttag
Daniel Jackson (supervisor)
Martin Rinard

For more information please contact: Dan Wilson, 617-253-1550,
dwilson at csail.mit.edu 
_______________________________________________
Seminars mailing list
Seminars at csail.mit.edu
http://lists.lcs.mit.edu/mailman/listinfo/seminars



More information about the PRL mailing list