What is Salsa?
Salsa is an invariant checker for specifications in SAL (the SCR Abstract
Language). To establish a formula as an invariant without any user guidance,
Salsa carries out an induction proof that utilizes tightly integrated decision
procedures (currently a combination of BDD algorithms and a constraint solver
for integer linear arithmetic) for discharging the verification
conditions. The user interface of Salsa is designed to mimic the interfaces of
model checkers; i.e., given a formula and a system description, Salsa either
establishes the formula as an invariant of the system (but returns no proof)
or provides a counterexample. In either case, the algorithm will
terminate. Unlike model checkers, Salsa returns a state pair as a
counterexample and not an execution sequence. Also, due to the incompleteness
of induction, users must validate the counterexamples. The use of induction
enables Salsa to combat the state explosion problem that plagues model
checkers -- it can handle specifications whose state spaces are too large for
model checkers to analyze. Also, unlike general purpose theorem
provers, Salsa concentrates on a single task and gains efficiency
by employing a set of optimized heuristics.
Example SAL Specifications
Papers
-
R. Bharadwaj and S. Sims.
"Salsa: Combining constraint solvers with bdds for automatic invariant
checking."
In Tools and Algorithms for the Construction and Analysis of
Systems (TACAS '00), Berlin, March 2000. Springer-Verlag.
[ .pdf ]
Patents
-
United States Patent 7,058,910 titled "Invariant Checking Method and
Apparatus using Binary Decision Diagrams in Combination with Constraint
Solvers" issued June 6, 2006.
Contact
Salsa was built by Ramesh Bharadwaj
and Steve Sims.
Acknowledgments
The Salsa team would like to thank the Office of Naval Research for their
funding of this project. Much of the work of Sims on this project was carried
out at the U.S. Naval Research Laboratory where Bharadwaj is a researcher. We
also thank Connie Heitmeyer, Ralph Jeffords, Myla Archer, Jim Kirby, Bruce
Labaw, Susanne Graf, and several anonymous referees for their valuable
comments on Salsa.
|