Tuesday 6 November 2007, Atlanta, Georgia, USA

In association with the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007)

o  Workshop Description
o  Workshop Committee
o  Workshop Program
o  Abstracts
o  Proceedings
o  Workshop Location
o  Contacts

This was the second in the Automated Formal Methods (AFM) workshop series, which began with AFM06. 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.

 *NEW* We are pleased to announce that AFM08 will be held in association with CAV in Princeton NJ; the tentative date is 14 July 2008.

Workshop Description

This one-day workshop was 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 (rather than the construction) 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.

Workshop Program

The full program included nine contributed papers (listed below) selected by the international program committee, brief descriptions of new developments in the SRI tool suite, and short presentations (five minutes, five slides) on ongoing work from the user community.

8:45-9:00 Welcome
9:00-9:30 Keynote Address: SMT @ Microsoft  (slides)
Leonardo de Moura, Microsoft Research.
9:30-10:00 Preliminary Explorations in Specifying and Validating Entity-Relationship Models in PVS
Venkatesh Choppella, Arijit Sengupta, Edward Robertson and Steve Johnson.
10:00-10:30 Topology in PVS
David Lester.
10:30-11:00 COFFEE BREAK
11:00-11:30 Model Checking for the Practical Verificationist: A User's Perspective on SAL
Lee Pike.
11:30-12:00 Modelling and test generation using SAL for interoperability testing in Consumer Electronics
Srikanth Mujjiga and Srihari Sukumaran.
12:00-12:30 Extended Interface Grammars for Automated Stub Generation  (slides)
Graham Hughes and Tevfik Bultan.
12:30-2:00 LUNCH
2:00-2:30 Cooperative Reasoning for Automatic Software Verification
Andrew Ireland.
2:30-3:00 Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant
Sylvain Conchon, Evelyne Contejean, Johannes Kanig and Stéphane Lescuyer.
3:00-3:30 Using SMT solvers to verify high-integrity programs
Paul Jackson, Bill James Ellis and Kathleen Sharp.
3:30-4:00 COFFEE
4:00-4:30 SMT-Based Synthesis of Distributed Systems
Bernd Finkbeiner and Sven Schewe.
4:30-5:00 Short Talks
From PVS to Java and Back Again
Cesar Munoz
Measured Boot Model  (slides)
J. Millen (with J. Guttman, J. Ramsdell, J. Sheehy, B. Sniffen, L. Spriggs)
Verify the requirements for large telecommunications systems
Thomas Weigert
Hierarchical Specifications
Rance DeLong
5:00-6:00 Discussion of Open Source Development and Enhancements for PVS and SAL.


Leonardo de Moura, Microsoft Research
SMT @ Microsoft
Abstract: Decision procedures for checking satisfiability of logical formulas are crucial for many verification applications. Of particular recent interest are solvers for Satisfiability Modulo Theories (SMT). The success of SMT is largely due to the supported background theories: uninterpreted functions; real or integer arithmetic; and theories of program or hardware structures such as bit-vectors and arrays.

SMT solvers are used in several projects at Microsoft, the main applications are: program verification, test case generation, whitebox fuzz testing, predicate abstraction, and internet worm prevention. In this talk, we will describe these projects, their requirements, and how they influenced the design and implementation of SMT solvers.

Thomas Weigert
Verify the requirements for large telecommunications systems

Abstract: The most expensive failures of computer-based systems are due to unanticipated interactions between system components. In telecommunications systems, this problem has long been known as the "feature interaction problem" and a series of conferences is dedicated to developing solutions to this costly source of errors. With the advent of more sophisticated user interactions, this problem has spread to web services, email systems, user interfaces for consumer devices, and many more.

While a number of research approaches to solving the feature interaction problem have been presented, these have not significantly impacted industrial system development. We believe, this is due to that the mathematical representations chosen to model system behavior have pushed solutions towards formalisms that are inaccessible to the majority of engineers and also towards implementations that are not able to cope with the enormous state spaces induced by todayls computer systems.

We have implemented a verification system based on an alternative mathematical model of behavior (Letichevsky's theory of agents and environments) and have been able to express popular engineering notations such as UML sequence diagrams within this framework in a manner that allows efficient reasoning over such specifications. Our tool has been successfully deployed to prove the correctness of large, industrial-scale system specifications and which has been able to detect serious defects in each of these specifications. Detecting such defects before implementation promises a dramatic reduction in the cost of quality of large software-based systems.

Workshop Proceedings

The proceedings will be published by ACM. A preprint is available (PDF).

Workshop Committee

Tevfik BultanUC Santa Barbara
Jin Song DongNational University of Singapore
Bernd FinkbeinerUniversitat des Saarlandes
Marsha ChechikUniversity of Toronto
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
Joe KiniryUniversity College Dublin
Pete ManoliosGeorgia Tech
David MonniauxVerimag
Paul MinerNASA Langley Research Center
Leonardo de MouraMicrosoft Research
David NaumannStevens Institute of Technology
Paritosh PandyaTIFR and IIT Mumbai
Andras PatariczaBudapest University of Technology and Economics
John PenixGoogle Inc
Lee PikeGalois Inc
S. RameshGeneral Motors Research
Scott StollerSUNY Stony Brook
Ofer StrichmanThe Technion
Neeraj SuriTU Darmstadt
Mark UttingWaikato University
Michael WhalenRockwell Collins Inc
Brian WilliamsMIT

Workshop Location

The workshop is colocated with ASE 2007 in Atlanta, Georgia at the Crowne Plaza Atlanta Buckhead

Workshop Organizers

John Rushby and N. Shankar, SRI International