[an error occurred while processing this directive]
PVS - Yices - SAL - FM

AFM09 (Automated Formal Methods)

June 27 2009, Grenoble, France

In association with the 21st International Conference on Computer Aided Verification (CAV 2009)

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

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.

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.

Workshop Program

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


Challenges in analyzing binary programs
Hassen Saïdi

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.

Contracts for the component-based design of embedded and distributed systems
Susanne Graf
Distributed, real-time and embedded systems usually multiple layers from the high-level functional layers down to the interaction with hardware. The design of such systems leads to complex hierarchical architectures with components subject to multiple constraints. The BIP composition operators allow specifying complex multi-party interactions between components in a hierarchical fashion, and by separating component behaviour and interaction between components. It is expressive enough to describe the interaction of a set of peers so as to abstract lower layers as composition operator represented by a set of connectors and their interactions. We define a notion of contract associated with components which strictly separates an expectation which it may have on the environment, called assumption, and a promise which is behaviour of the component under consideration that the environment may take for granted as long as it respects the component's expectation. Contrary to most notions of contracts, it does not express the assumptions directly on the component's interface but as a constraint on it's peers to which it is connected by a rich connectors as in BIP. We do not intend contracts to be used for compositional verification but rather for compositional design and independent implementation of components. Assumptions allow simplifying component implementations by relying on properties ensured by the environment. An interesting of our kind of contracts is to allow expressing also assumptions which need not to be expressible on the component's interface. This means that the component interfaces need not to be "artificially" enriched with analysis related attributes. Moreover, knowledge about peers and about lower layers is clearly separated, and specifications of lower layers, represented by a set of connectors, may be refined independently of components. So far, we have shown that this general contract framework is indeed a generalization of all existing notions of interface specifications or contracts that we have studied and proposed some general methodology. Here, we propose also a set of useful concepts which can be used to actually express contracts for components which must comply to safey and progress constraints.

Continuous Model.Driven Engineering - Formal Methods at the Application Level
Bernhard Steffen

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.

Why - an intermediate language for deductive program verification
Jean-Christophe Filliâtre

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.

Workshop Proceedings

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

Workshop Committee

Myla ArcherNaval Research Laboratory
Saddek BensalemVerimag
Aaron BradleyUniversity of Colorado, Boulder
Supratik ChakraborthyIIT Mumbai
Rance de LongTrusted Systems Laboratories
Leonardo de MouraMicrosoft Research
Jean-Christophe FilliâtreUniversite Paris Sud
Bernd FinkbeinerSaarbruecken University
Mike GordonCambridge University
John HarrisonIntel
Peter ManoliosNortheastern University
David MonniauxVerimag
David NaumannStevens Institute of Technology
Corina PasareanuNASA Ames
Lee PikeGalois Inc
Kazuhiro OgataJAIST
Sanjit SeshiaUC Berkeley
Ofer StrichmanThe Technion

Workshop Location

The workshop is colocated with CAV 2009 in Grenoble, France

Workshop Organizers

Hassen Saïdi and N. Shankar, SRI International

PVS - Yices - SAL - FM

Last modified: Tue 25 May 2021 02:25 PDT