FLoC 2006

AFM 2006

Automated Formal Methods
Seattle, August 21, 2006

AFM on Monday, August 21st

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

09:00‑09:30   John Rushby (SRI)
Overview of PVS, ICS, and SAL, and plans for the future [pdf]

09:30‑10:00   Sam Owre (SRI)
Recent PVS Language Developments [pdf]

10:00‑10:30   N. Shankar (SRI)
Recent PVS Prover Developments [pdf]

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

11:00‑11:30   Leonardo de Moura (SRI)
Overview of ICS/Yices [pdf]

11:30‑12:00   John Rushby (SRI)
Overview of SAL: Model Checking and Test Generation [pdf]

12:00‑12:30   Bruno Dutertre (SRI)
Model Checking Infinite-state Systems in SAL [pdf]

14:00‑15:00 Joseph Kiniry (School of Computer Science and Informatics, University College Dublin, Dublin, Ireland)
(Deeply) Integrating Programming and Proving [pdf]
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 (http://mobius.inria.fr/).

15:00‑15:30 Cesar Munoz
Batch Proving and Proof Scripting in PVS [pdf]