| AFM 2006 | Automated Formal Methods Seattle, August 21, 2006 |
Program
All sessions will take place in Suite 3228 unless otherwise indicated.
Monday, August 21st
Monday's program is also available with abstracts or side by side with other meetings.
09:00‑10:30 Session 1: Overview and PVS Developments
| 09:00 | John Rushby (SRI) Overview of PVS, ICS, and SAL, and plans for the future [pdf] |
| 09:30 | Sam Owre (SRI) Recent PVS Language Developments [pdf] |
| 10:00 | N. Shankar (SRI) Recent PVS Prover Developments [pdf] |
10:30‑11:00 Break
11:00‑12:30 Session 2: ICS/Yices and SAL
| 11:00 | Leonardo de Moura (SRI) Overview of ICS/Yices [pdf] |
| 11:30 | John Rushby (SRI) Overview of SAL: Model Checking and Test Generation [pdf] |
| 12:00 | Bruno Dutertre (SRI) Model Checking Infinite-state Systems in SAL [pdf] |
12:30‑14:00 Lunch break
14:00‑15:30 Session 3
| 14:00 | Joseph Kiniry (School of Computer Science and Informatics, University College Dublin, Dublin, Ireland) (Deeply) Integrating Programming and Proving [pdf] |
| 15:00 | Cesar Munoz Batch Proving and Proof Scripting in PVS [pdf] |
15:30‑16:00 Break
16:00‑18:00 Session 4
| 16:00 | Chris George and Anne E. Haxthausen Specification and Proof of the Mondex Electronic Purse |
| 16:30 | Borzoo Bonakdarpour and Sandeep S. Kulkarni Mechanical Verification of Automated Synthesis of Multitolerance |
| 17:00 | Paul Nicholas Loewenstein, Shailender Chaudhry, Robert Cypher and Chaiyasit Manovit Multiprocessor Memory Model Verification |
| 17:30 | Sam Owre Random Testing in PVS |
