|
SAL: Symbolic Analysis Laboratory
Natarajan Shankar
Abstract
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.
|