From LFM 2000: Fifth NASA Langley Formal Methods Workshop.
Edited by C. Michael Holloway.
NASA Langley Research Center, Hampton, VA.
June, 2000.
Pages 187–196.

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.

@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/}
}

• lfm2000.ps.gz