| || || || || |
An Overview of SAL
by Sam Owre, Dr. John Rushby, Dr. Hassen Saïdi, Dr. Natarajan Shankar, Dr. Ashish Tiwari, Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, César Muñoz, Harald Rueß, Vlad Rusu & Eli Singerman.
To become practical for assurance, automated formal
methods must be made more scalable, automatic,
and cost-effective. Such an increase in scope, scale, automation,
and utility can be derived from an emphasis on
a systematic separation of concerns during verification.
SAL (Symbolic Analysis Laboratory) attempts to address
these issues. It is a framework for combining different
tools to calculate properties of concurrent systems.
The heart of SAL is a language, developed in collaboration
with Stanford, Berkeley, and Verimag, for specifying
concurrent systems in a compositional way. Our instantiation
of the SAL framework augments PVS with tools
for abstraction, invariant generation, program analysis
(such as slicing), theorem proving, and model checking
to separate concerns as well as calculate properties (i.e.,
perform symbolic analysis) of concurrent systems. We
describe the motivation, the language, the tools, their
integration in SAL/PVS, and some preliminary experience
of their use.