Workshop on Model Checking and Program Analysis
Joint work with Mandana Vaziri

I presented a new method for finding bugs in code using SAT. The
code of a procedure is translated into an Alloy formula. A second
formula is obtained by combining this formula with a user-defined
specification, whose models are executions of the procedure that
violate the spec. The Alcoa checker is then used to find models. I
illustrated the use of this method to find shape analysis bugs in
a benchmark suite of programs used previously by Sagiv et al. The
method is not sound, since it may miss bugs, but is complete
(so long as datatypes aren't abstracted). The merit of the approach
is its ability to handle user-defined specs, not only to check code
against, but also as surrogates for called procedures.

slides