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