An Overview of SAL

Authors

Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, C�sar Mu�oz, Sam Owre, Harald Rue�, John Rushby, Vlad Rusu, Hassen Sa�di, N. Shankar, Eli Singerman, and Ashish Tiwari

Abstract

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.

gzipped postscript

BibTeX Entry

@inproceedings{SALoverview00:LFM,
    AUTHOR = {Saddek Bensalem and Vijay Ganesh and Yassine Lakhnech and C\'{e}sar Mu\~{n}oz and Sam Owre and Harald Rue\ss and John Rushby and Vlad Rusu and Hassen Sa\"{i}di and {N.} Shankar and Eli Singerman and Ashish Tiwari},
    TITLE = {An Overview of {SAL}},
    BOOKTITLE = {{LFM} 2000: Fifth {NASA} Langley Formal Methods Workshop},
    YEAR = {2000},
    EDITOR = {{C.} Michael Holloway},
    PAGES = {187--196},
    ADDRESS = {Hampton, {VA}},
    MONTH = {jun},
    ORGANIZATION = {{NASA} Langley Research Center},
    URL = {http://www.csl.sri.com/papers/lfm2000/}
}

Sam Owre: owre@csl.sri.com