August 21, 2006, in association with FLoC, Seattle

This was a one-day workshop on Integrated Formal Methods based around the SRI tools PVS, SAL, and Yices. The workshop included a half-day tutorial on the novel and advanced features of these systems, and another half-day session devoted to contributed talks.

The contributed session included talks from within the user community of PVS, SAL, and Yices. These contributions reported on experiments carried out with these tools, experience integrating these tools into other systems, and comparisons with other comparable tools.


Session 1: Overview and PVS Developments (09:00‑10:30)

09:00‑09:30   John Rushby (SRI)
Overview of PVS, SAL, and Yices and plans for the future   
09:30‑10:00   Sam Owre (SRI)
Recent PVS Language Developments   
10:00‑10:30   N. Shankar (SRI)
Recent PVS Prover Developments   

Break (10:30‑11:00)

Session 2: Yices and SAL (11:00‑12:30)

11:00‑11:30   Leonardo de Moura (SRI)
Overview of Yices   
11:30‑12:00   John Rushby (SRI)
Overview of SAL: Model Checking and Test Generation   
12:00‑12:30   Bruno Dutertre (SRI)
Model Checking Infinite-state Systems in SAL   
(slides , examples)

Lunch break (12:30‑14:00)

Session 3 (14:00‑15:30)

14:00‑15:00   Joseph Kiniry (invited speaker)
(Deeply) Integrating Programming and Proving   
Automatic and interactive theorem provers (ITPs) and interactive development environments (IDE) are two beasts that historically come from disparate communities, have different goals, and rarely interact, but focus on similar kinds of artifacts. Only occasionally have (human) provers been programmers, and even more rarely have programmers been provers. Recently, these two disciplines have been increasingly integrated, in both practical and theoretical ways, as practical program verification becomes more feasible, fast, and fun. We will summarize some of our initial experiments in "borrowing" some of the best ideas from modern IDEs for ITPs and discuss next steps in more deeply integrating proving and programming in the context of the Mobius project (
15:00‑15:30   Cesar Munoz
Batch Proving and Proof Scripting in PVS   
(slides. paper)

Break (15:30‑16:00)

Session 4 (16:00‑18:00)

16:00‑16:30   Chris George and Anne E. Haxthausen
Specification and Proof of the Mondex Electronic Purse   
(slides, paper)
16:30‑17:00   Borzoo Bonakdarpour and Sandeep S. Kulkarni
Towards Reusing Formal Proofs for Verification of Fault-Tolerance   
(slides, paper)
17:00‑17:30   Paul Nicholas Loewenstein, Shailender Chaudhry, Robert Cypher and Chaiyasit Manovit
Multiprocessor Memory Model Verification   
(slides, paper)
17:30‑18:00   Sam Owre
Random Testing in PVS   
(slides, paper)

The Tools

PVS, SAL, and Yices are available under license from SRI; there is no charge for research and educational use.

More papers on formal methods and automated verification by SRI authors be found at