Sciweavers

TACAS
2000
Springer

Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking

13 years 10 months ago
Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking
Salsa is an invariant checker for speci cations 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 veri cation 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 speci cations whose sta...
Ramesh Bharadwaj, Steve Sims
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where TACAS
Authors Ramesh Bharadwaj, Steve Sims
Comments (0)