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


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

	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