An Overview of SAL

摘要: To become practical for assurance, automated formal methods must be made more scalable, automatic, and cost-effective. Such an increase in scope, scale, automation, utility can derived from emphasis on a systematic separation of concerns during verification. SAL (Symbolic Analysis Laboratory) attempts to address these issues. It is framework combining different tools calculate properties concurrent systems. The heart language, developed collaboration with Stanford, Berkeley, Verimag specifying systems compositional way. Our instantiation the augments PVS abstraction, invariant generation, program analysis (such as slicing), theorem proving, model checking separate well (i.e., perform, symbolic analysis) We. describe motivation, tools, their integration SAL/PAS, some preliminary experience use.