SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

An Overview of SAL
 by Sam Owre, Dr. Harald Rue▀, Dr. John Rushby, Dr. Hassen Sa´di, Dr. Natarajan Shankar, Dr. Ashish Tiwari, Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, César Muñoz, Vlad Rusu & Eli Singerman.

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.


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.
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/}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy