SAL 2

Abstract

SAL (see http://sal.csl.sri.com) is an open suite of tools for analysis of state machines; it constitutes part of our vision for a Symbolic Analysis Laboratory that will eventually encompass SAL, the PVS verification system, the ICS decision procedures, and other tools developed in our group and elsewhere.SAL provides a language similar to that of PVS, but specialized for the specification of state machines; it was first released with an explicit-state model checker as SAL 1 in July 2002; SAL 2, which was released in December 2003, adds high-performance symbolic and bounded model checkers, and novel infinite bounded and witness model checkers. Both the bounded model checkers can additionally perform verification by k-induction, and the capabilities of all the model checkers and their components are available through an API that is scriptable in Scheme.