SAL 2

Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, N. Shankar, Maria Sorea, and Ashish Tiwari

Tool description to be presented at CAV 2004. 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 {\em infinite bounded} and {\em 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.

gzipped postscript, or postscript or PDF

BibTeX Entry

 @InProceedings{SAL-cav04,
  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},
  booktitle = {Proceedings of the 16th International Conference on 
               Computer Aided Verification (CAV)},
  year =      {2004},
  series =    {LNCS},
  address =   {Boston},
  month =     {July},
  publisher = {Springer Verlag},
  note =      {Tool description},
}