|
This will be the fourth in the Automated Formal Methods (AFM) workshop series, following on from AFM06, AFM07, and AFM08. 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 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 program includes six contributed papers and four invited tutorials selected by the international program committee.
| 9:00 | Empty (SPIN has invited talk by Joseph Sifakis; RV has invited talk by Sriram Rajamani) |
| 10:30 | A Test Generation Framework for Distributed
Fault-Tolerant Algorithms Alwyn Goodloe, Corina Pasareanu, David Bushnell and Paul Miner. |
| 10:55 | Automatic Synthesis of an Efficient
Algorithm for the Similarity of Strings Problem Luca Chiarabini |
| 11:20 | Formalizing Meta-Routing in PVS Anduo Wang and Boon Thau Loo. |
| 11:45 | Invited tutorial: Challenges in analyzing
binary programs Hassen Saïdi |
| 12:30 | Lunch |
| 2:00 | Invited tutorial: Contracts for the
component-based design of embedded and distributed systems Susanne Graf |
| 2:45 | Invited tutorial: Continuous Model.Driven
Engineering - Formal Methods at the Application Bernhard Steffen |
| 3:30 | Coffee |
| 4:00 | SAL, Kodkod, and BDDs for Validation of B
Models Ilya Lopatkin, Daniel Plagge, Alexei Iliasov, Michael Leuschel and Alexander Romanovsky. |
| 4:25 | Model-Checking Modulo Theories at Work: The
integration of Yices in MCMT Silvio Ghilardi and Silvio Ranise |
| 4:50 | Graph-based Reduction of Program Verification
Conditions Jean-Francois Couchot, Alain Giorgetti and Nicolas Stouls |
| 5:15 | Invited tutorial: Why - an intermediate
language for deductive program verification Jean-Christophe Filliâtre |
| 6:00 | Close of Workshop |
Program analysis is an enough challenging task when source code is available. It is even more challenging when neither the source code nor debug information is present. The analysis task is further hindered when the available binary code has been obfuscated to prevent the analysis from being carried out. In this presentation, we review the main challenges when analyzing binary programs and explore techniques for recovery of information that allows program understanding and reverse-engineering. We illustrate these techniques on the Conficker worm that has plagued the Internet in the past few months.
Agility is a must, in particular for business-critical applications. Complex systems and processes must be continuously updated in order to meet the ever changing market conditions. Continuous Model Driven Engineering addresses this need by by continuously involving the customer/application expert throughout the whole systems? life cycle including maintenance and evolution. Conceptually, it is based on the One Thing Approach (OTA), which combines the simplicity of the waterfall development paradigm with a maximum of agility. The key to OTA is to view the whole development process simply as a complex hierarchical and interactive decision process, where each stakeholder, including the application expert, is allowed to continuously place his/her decisions in term of constraints. Thus semantically, at any time, the state of the development or evolution process can simply be regarded as the current set of constraints, and each development or evolution step can be regarded simply as a transformation of this very constraint set. This approach, conceptually, allows one 1) to monitor globally and at any time the consistency of the development or evolution process simply via constraint checking, and 2) to impose a kind of decision hierarchy by mapping areas of ompetencies to roles of individuals, in order to identify required actions in case of constraint violation. The essence and power of this approach, which is technically supported by the jABC development and execution framework, will be illustrated along real life application scenarios.
This tutorial is an introduction to the Why tool, an intermediate language for deductive program verification. The purpose of the Why tool is two-fold: first, it computes weakest preconditions for a small alias-free programming language, which is designed to be the target of other verification tools for languages such as C or Java; second, it translates verification conditions into the native languages of several existing theorem provers, either automatic such as Simplify, Alt-Ergo, Yices, Z3, etc. or interactive such as Coq, PVS, Isabelle, etc. Why is currently used in several verification frameworks such as Caduceus, Krakatoa, or Frama-C.
| Myla Archer | Naval Research Laboratory |
| Saddek Bensalem | Verimag |
| Aaron Bradley | University of Colorado, Boulder |
| Supratik Chakraborthy | IIT Mumbai |
| Rance de Long | Trusted Systems Laboratories |
| Leonardo de Moura | Microsoft Research |
| Jean-Christophe Filliâtre | Universite Paris Sud |
| Bernd Finkbeiner | Saarbruecken University |
| Mike Gordon | Cambridge University |
| John Harrison | Intel |
| Peter Manolios | Northeastern University |
| David Monniaux | Verimag |
| David Naumann | Stevens Institute of Technology |
| Corina Pasareanu | NASA Ames |
| Lee Pike | Galois Inc |
| Kazuhiro Ogata | JAIST |
| Sanjit Seshia | UC Berkeley |
| Ofer Strichman | The Technion |
