Important dates

abstracts: May 21
full papers: May 28
notification: July 4
final version: July 23
early registration: Sept 15
conference: October 11-14


Satellite events of iFM 2010

The regular iFM conference starts on Tuesday, October 12. Monday, October 11, is devoted to the following events that are of interest to the iFM community. Although you can register separately for the main conference and these satellite events, preferred rates are available for joint registration.

Note: The tutorials will last half a day each so that participants can attend both of them.

WTS 2010: Workshop on Formal Methods for Web Data Trust and Security

An increasing number of web applications use XML as their data model or as a format to export other data, including in particular user content exchange applications (social networks, mashups, blogs, photo sharing sites, wikis...) for which privacy is a central issue. In this context, it is critical to investigate the problem of access control for XML documents.

The workshop WTS aims at bringing together people interested in formal models for security and access control for Web data exchange and foster collaboration amongst those working in formal methods, system verification, access control for Web data, and computer security and privacy.

Tutorial: Verification of C# programs using Spec# and Boogie 2

(Rosemary Monahan, slides, examples)

In this tutorial we present the Spec# Programming System, the verifier for Spec# programs. Throughout our presentation we illustrate how the Spec# Programming System can be used to verify programs in an object-oriented environment. The effect will be two-fold: participants will be given the practical experience of using the Spec# Programming System and they will learn about Boogie 2, the intermediate representation language that Spec# programs are translated to before verification. Through this knowledge participants will develop an understanding of how logical verification conditions are generated in program verification tools.

Tutorial: The TLA+ Proof System

(Denis Cousineau, Stephan Merz, slides, examples)

The TLA+ Proof System (TLAPS) is a platform for computerized verification of TLA+ proofs using formal reasoning systems such as automated theorem provers, proof-assistants, SMT/SAT solvers, and decision procedures. TLA+ is a specification language designed for concurrent, distributed, reactive and real-time systems, but it can also be used to formalize any discrete algorithm. The TLA+ proof language is declarative, hierarchical, and scalable to large system specifications. It provides a consistent abstraction over the various “backend” verifiers. The current release of TLAPS handles just enough temporal reasoning to check safety properties; an extension to the full TLA+ language is under active development.

The tutorial will present the design of the proof language and the architecture of the TLAPS. Participants will learn how to use the system to carry out proofs of elementary safety properties, such as invariants and step simulation.