AFM09 Program and Abstracts

[Sam Owre]

    Fourth Workshop on Automated Formal Methods
       (http://fm.csl.sri.com/afm09)
       In association with CAV 2009 (http://www-cav2009.imag.fr/)
         June 27, 2009
         Grenoble, France

9:00   :  Empty (SPIN has invited talk by Joseph Sifakis;
                 RV has invited talk by Sriram Rajamani)

                       
10:30  :  Alwyn Goodloe, Corina Pasareanu, David Bushnell and Paul Miner.
          A Test Generation Framework for Distributed Fault-Tolerant
          Algorithms
10:55  :  Luca Chiarabini.
          Automatic Synthesis of an Efficient Algorithm for the
	  Similarity of Strings Problem
11:20  :  Anduo Wang and Boon Thau Loo.
          Formalizing Meta-Routing in PVS
11:45  :  Hassen Saidi
          Challenges in analyzing binary programs (Invited tutorial)

12:30  :  Lunch

2:00   :  Susanne Graf
          Contracts for the component-based design of embedded and
          distributed systems (Invited tutorial)
2:45   :  Bernhard Steffen
          Continuous Model.Driven Engineering -
	    Formal Methods at the Application  (Invited tutorial)
3:30   :  Coffee
4:00   :  Ilya Lopatkin, Daniel Plagge, Alexei Iliasov, Michael Leuschel and
             Alexander Romanovsky.
	  SAL, Kodkod, and BDDs for Validation of B Models
4:25   :  Silvio Ghilardi and Silvio Ranise
          Model-Checking Modulo Theories at Work: The integration of Yices
          in MCMT
4:50   :  Jean-Francois Couchot, Alain Giorgetti and Nicolas Stouls
          Graph-based Reduction of Program Verification Conditions
5:15   :  Jean-Francois Filliatre
          Why - an intermediate language for deductive program verification
	    (Invited tutorial)
6:00   :  Close	of Workshop

Abstracts
Title: Challenges in analyzing binary programs
Speaker: Hassen Saidi (SRI Computer Science Laboratory)

Abstract: 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.

Title: Contracts for the component-based design of embedded and distributed
       systems 
Speaker: Susanne Graf

Abstract: 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 hierachical
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 generalisation 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.


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

Abstract: 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.

Title: Why - an intermediate language for deductive program verification
Speaker: Jean Christophe Filliatre

Abstract: 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.