Monday 14 July 2008, Princeton, New Jersey, USA

In association with the 20th International Conference on Computer Aided Verification (CAV 2008)

o  Workshop Description
o  Workshop Committee
o  Invited Speaker
o  Workshop Program
o  Proceedings
o  Workshop Location
o  Contacts

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.


AFM08 will be held in Room 006 of the Friend Center on the Princeton Campus. Directions and parking permit are here.

Workshop Description

This one-day workshop will be centered around, but not exclusive to, the SRI suite of tools (PVS, SAL and HybridSAL, and Yices), and experiences and experiments involving the application, integration, and extension of these and similar tools.

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.

Important Dates

Submissions due25 May 2008
Author notification13 June 2008
CAV registration21 June 2008
Camera ready copy due7 July 2008
AFM08 Workshop14 July 2008

Invited Speaker

We are delighted that Gregoire Hamon of Mathworks will present an invited talk:
Simulink Design Verifier--Applying Automated Formal Methods to Simulink and Stateflow

Workshop Program

The program includes an invited paper and six contributed papers selected by the international program committee. Responding to requests at previous workshops, each block of talks is preceded by a mini-tutorial on the technology and the tool related to those talks.

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).

AFM08 will be held in Room 006 of the Friend Center on the Princeton Campus.
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

Workshop Proceedings

The Proceedings will be published in the ACM digital library.
The preprint proceedings are available here (pdf).

And here are the proceedings from AFM07.

Workshop Committee

Aaron BradleyUniversity of Colorado, Boulder
Supratik ChakrabortyIIT Mumbai
Bernd FinkbeinerUniversitat des Saarlandes
Jean-Christophe FilliatreUniversite Paris Sud
Marcelo FriasUniversidad de Buenos Aires
Chris GeorgeUnited Nations University IIST
Mike GordonCambridge University
Constance HeitmeyerNaval Research Laboratory
Paul JacksonEdinburgh University
Steve JohnsonIndiana University
Leonardo de MouraMicrosoft Research
Pete ManoliosNortheastern University
David MonniauxVerimag
Cesar MunozNational Institute of Aerospace
David NaumannStevens Institute of Technology
Kazuhiro OgataJAIST
Corina PasareanuNASA Ames
Lee PikeGalois Inc
Koushik SenUniversity of California, Berkeley
Maria SoreaEADS
Ofer StrichmanThe Technion
Mark UttingWaikato University
Michael WhalenRockwell Collins Inc

Workshop Location

The workshop is colocated with CAV 2008 in Princeton, New Jersey

AFM08 will be held in Room 006 of the Friend Center on the Princeton Campus. Directions and parking permit are here.

Workshop Organizers

John Rushby and N. Shankar, SRI International