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.
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.
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.
|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|
Model Checking for the Practical Verificationist: A User's Perspective on
|11:30-12:00||Modelling and test generation using SAL for interoperability testing in
Srikanth Mujjiga and Srihari Sukumaran.
|12:00-12:30||Extended Interface Grammars for Automated Stub Generation (slides)|
Graham Hughes and Tevfik Bultan.
|2:00-2:30||Cooperative Reasoning for Automatic Software Verification|
|2:30-3:00||Lightweight Integration of the Ergo Theorem Prover inside a Proof
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.
|4:00-4:30||SMT-Based Synthesis of Distributed Systems|
Bernd Finkbeiner and Sven Schewe.
|5:00-6:00||Discussion of Open Source Development and Enhancements for PVS and SAL.|
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.
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.
|Tevfik Bultan||UC Santa Barbara|
|Jin Song Dong||National University of Singapore|
|Bernd Finkbeiner||Universitat des Saarlandes|
|Marsha Chechik||University of Toronto|
|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|
|Joe Kiniry||University College Dublin|
|Pete Manolios||Georgia Tech|
|Paul Miner||NASA Langley Research Center|
|Leonardo de Moura||Microsoft Research|
|David Naumann||Stevens Institute of Technology|
|Paritosh Pandya||TIFR and IIT Mumbai|
|Andras Pataricza||Budapest University of Technology and Economics|
|John Penix||Google Inc|
|Lee Pike||Galois Inc|
|S. Ramesh||General Motors Research|
|Scott Stoller||SUNY Stony Brook|
|Ofer Strichman||The Technion|
|Neeraj Suri||TU Darmstadt|
|Mark Utting||Waikato University|
|Michael Whalen||Rockwell Collins Inc|