|
This will be the third in the Automated Formal Methods (AFM) workshop series, following on from AFM06 and AFM07. AFM functions both as a user's meeting for the SRI tools PVS, SAL (with HybridSAL), and Yices, and as a general workshop for those interested in state of the art automation for formal methods. VenueAFM08 will be held in Room 006 of the Friend Center on the Princeton Campus. Directions and parking permit are here. |
AFM is particularly interested in the use of highly automated tools for formal methods and the tight or loose integration of different methods into tool chains that strive to provide end-to-end automation for all aspects of software development. Users of all levels of expertise are invited to report on their experiences.
We hope that AFM will provide a rewarding forum for presentation of interesting work and new ideas in the application and integration of highly automated formal methods, with stimulating and provocative discussion of successes, failures, and new directions.
The workshop will focus on submitted contributions, including a session for short presentations (five minutes, five slides), but may include invited speakers or a tutorial on the recent developments in SRI's or similar tools if time permits.
| Submissions due | 25 May 2008 |
| Author notification | 13 June 2008 |
| CAV registration | 21 June 2008 |
| Camera ready copy due | 7 July 2008 |
| AFM08 Workshop | 14 July 2008 |
There is session for short talks on ongoing work or discussion of other topics of interest. Please contact the organizers (by email or in person) if you wish to make a presentation in this session (five minutes, five slides).
| 9:00-9:15 | Welcome and Introduction |
| 9:15-10:00 | Invited talk:Simulink Design Verifier--Applying
Automated Formal Methods to Simulink and Stateflow
Gregoire Hamon |
| 10:00-10:30 | Mini-tutorial: SMT Solving and Yices
Bruno Dutertre |
| 10:30-11:00 | BREAK |
| 11:00-11:30 | Using Yices as an Automated Solver in Isabelle/HOL
(slides) Levent Erkok and John Matthews |
| 11:30-12:00 | Automated Proof with Caduceus: Recent Industrial Experience
(slides) Daniel Sheridan |
| 12:00-12:30 | Detecting Erroneous Assumptions When Verifying Software Using SMT Solvers
(slides) David Cok |
| 12:30-2:00 | LUNCH |
| 2:00-2:30 | Mini-tutorial: Model Checking and SAL
John Rushby |
| 2:30-3:00 | Strengthened State Transitions for
Invariant Verification in Practical Depth-Induction
Peter Bokor, Sandeep Shukla, Andras Pataricza and Neeraj Suri |
| 3:00-3:30 | Using SRI SAL Model Checker for
Combinatorial Tests Generation in the Presence of Temporal
Constraints
Andrea Calvagna and Angelo Gargantini |
| 3:30-4:00 | BREAK |
| 4:00-4:30 | Mini-tutorial: Theorem Proving and PVS
N. Shankar |
| 4:30-5:00 | A Case Study in Automated Verification
(slides) Jason Kirschenbaum, Heather Harton and Murali Sitaraman |
| 5:00-5:30 | Short papers and discussion
|
| 5:30 | Wrapup and adjourn |
And here are the proceedings from AFM07.
| Aaron Bradley | University of Colorado, Boulder |
| Supratik Chakraborty | IIT Mumbai |
| Bernd Finkbeiner | Universitat des Saarlandes |
| Jean-Christophe Filliatre | Universite Paris Sud |
| Marcelo Frias | Universidad de Buenos Aires |
| Chris George | United Nations University IIST |
| Mike Gordon | Cambridge University |
| Constance Heitmeyer | Naval Research Laboratory |
| Paul Jackson | Edinburgh University |
| Steve Johnson | Indiana University |
| Leonardo de Moura | Microsoft Research |
| Pete Manolios | Northeastern University |
| David Monniaux | Verimag |
| Cesar Munoz | National Institute of Aerospace |
| David Naumann | Stevens Institute of Technology |
| Kazuhiro Ogata | JAIST |
| Corina Pasareanu | NASA Ames |
| Lee Pike | Galois Inc |
| Koushik Sen | University of California, Berkeley |
| Maria Sorea | EADS |
| Ofer Strichman | The Technion |
| Mark Utting | Waikato University |
| Michael Whalen | Rockwell Collins Inc |
AFM08 will be held in Room 006 of the Friend Center on the Princeton Campus. Directions and parking permit are here.
