SAL: Symbolic Analysis Laboratory

Natarajan Shankar


SAL is a framework for combining theorem proving, model checking, and program analysis tools for the analysis of transition systems. SAL is based on an intermediate language for the modular description of transition systems. The intermediate language mediates the communication between different backend tools for verifying properties and for generating invariants and abstractions. We discuss the architecture of SAL, the syntax and semantics of its intermediate language, and the various functions for analyzing SAL transition systems. We will also present the relationship between SAL and the other verification tools developed at SRI such as PVS and ICS.

©2002-2018 U.C. Regents