[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