SAL 2
Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby,
N. Shankar, Maria Sorea, and Ashish Tiwari
Tool description presented at CAV 2004.
Appears in Springer Verlag LNCS 3114, pp. 496-500.
Copyright
Springer Verlag LNCS
Abstract
SAL 2 augments the specification language and explicit-state model
checker of SAL 1 with high-performance symbolic and bounded model
checkers, and with novel infinite bounded and witness
model checkers. The bounded model checker can use several different
SAT solvers, while the infinite bounded model checker similarly can
use several different ground decision procedures. SAL 2 provides a
scriptable API for its basic model checking and analysis functions
that can be used to extend the system. All four new model checkers
are implemented using this interface.
Its high-level specification language and wide range of model checkers
make SAL convenient for those seeking a ready-to-use solution, while
its scriptability and flexible choice of backend analyzers should make
it attractive to those seeking an experimental platform.
This is slightly expanded from the published version:
gzipped postscript,
or
plain postscript
or
PDF
or
crude ascii (for your Palm Pilot)
BibTeX Entry
@inproceedings{SAL2,
AUTHOR = {Leonardo de Moura and Sam Owre and Harald Rue{\ss} and John Rushby
and N. Shankar and Maria Sorea and Ashish Tiwari},
TITLE = {{SAL 2}},
PAGES = {496--500},
BOOKTITLE = {Computer-Aided Verification, {CAV} 2004},
EDITOR = {Rajeev Alur and Doron Peled},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
VOLUME = 3114,
ADDRESS = {Boston, MA},
MONTH = jul,
YEAR = 2004
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page