PVS • Yices • SAL • FM

AFM08 (Automated Formal Methods)

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  Important Dates
o  Electronic Submissions
o  Invited Speaker
o  Accepted Papers
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.

Venue (new)

AFM08 will be held in Room 006 of the Friend Center on the Princeton Campus. Directions and parking permit are here. We'll start at 9, take lunch 12:30 to 2, and finish at 5 or 5:30. The precise schedule will be posted shortly.

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

Electronic Submissions

Submissions in PDF format should be between 3-12 pages and follow the guidelines for ACM SIG Proceedings.

The AFM Easychair site is open for electronic submission of final versions of the accepted papers.

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

Accepted Papers

Strengthened State Transitions for Complete Invariant Verification in Practical Depth-Induction
Peter Bokor, Sandeep Shukla, Andras Pataricza and Neeraj Suri
Using SRI SAL Model Checker for Combinatorial Tests Generation in the Presence of Temporal Constraints
Andrea Calvagna and Angelo Gargantini
Detecting Erroneous Assumptions When Verifying Software Using SMT Solvers
David Cok
Using Yices as an Automated Solver in Isabelle/HOL
Levent Erkok and John Matthews
A Case Study in Automated Verification
Jason Kirschenbaum, Heather Harton and Murali Sitaraman
Automated Proof with Caduceus: Recent Industrial Experience
Daniel Sheridan

Workshop Proceedings

Proceedings will be published in the ACM digital library; here are the AFM07 proceedings. Preprint proceedings will be available on this site (here is the 2007 preprint[PDF]).

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

Workshop Organizers

John Rushby and N. Shankar, SRI International

PVS • Yices • SAL • FM

Last modified: Thu 03 Jul 2008 14:50 PDT