Wednesday November 5, 2003, 10:30-11:30, 4760 Boelter Hall.

Testing Based on a Solver for Executable Predicates

Darko Marinov
MIT CSAIL

An executable predicate is a piece of code that takes an input and
returns a boolean.  Writing a predicate that describes a set of test
inputs is usually much less work than writing a high-quality test
suite.  This talk presents Korat, our provably-correct solver for
executable predicates: given a predicate and a bound on the size of
predicate's inputs, Korat automatically generates all nonisomorphic
inputs for which the predicate returns true.  We have developed a
testing tool based on Korat for Java predicates, and the FSE group at
Microsoft Research has developed a tool based on Korat for the
Abstract State Machine Language predicates.  This talk also presents
how these tools have been applied to testing several libraries and
applications, including data structure implementations, a naming
architecture for mobile networks, a solver for declarative predicates,
and an XPath compiler.  The results indicate that it is feasible to
use exhaustive testing to obtain high-quality test suites that can
achieve high code coverage and detect subtle faults.

About the speaker:  Darko Marinov is a PhD student at the Computer
Science and Artificial Intelligence Laboratory, MIT, where he co-leads
the MulSaw project.  He received an SM from MIT for work on Credible
Compilation and a BS in Computer Science and Engineering from the
University of Belgrade, Yugoslavia.  His research interests include
specification languages and checking code conformance, both dynamically
(software testing, run-time verification), and statically (model
checking, theorem proving, program analysis).  More details can be
found online at:  http://cag.lcs.mit.edu/~marinov

Host: Jens Palsberg