July 14, 2010, Edinburgh

In association with Computer-Aided Verification (CAV) 2010, part of the Federated Logic Conference (FLoC)

This will be the fifth in the Automated Formal Methods (AFM) workshop series, following on from AFM06, AFM07, AFM08, and AFM09 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

AFM is a one-day workshop centered around the use and integration of formal verification tools for specification, interactive theorem proving, satisfiability (SAT) and satisfiability modulo theories (SMT), model checking, program verification, code generation, and testing, as well as interfaces, documentation, and education. This workshop was first initiated as a users' group meeting for the SRI formal verification tools such as PVS, SAL, and Yices, but the topics are not restricted to these tools. The first workshop was held at FLoC'06, the second workshop with ASE'07, and the third and forth workshops took place respectively in conjunction with CAV'08 and CAV'09.

We welcome position papers, research papers, and reports on work in progress on the topics listed above, particularly those that report on experiments, tool integration and evaluation, and case studies. Papers must be fewer than 8 pages long in the ACM SIG Proceedings style (http://www.acm.org/sigs/publications/proceedings-templates) and should be submitted to http://www.easychair.org/conferences/?conf=afm10).

Important Dates

Position papers dueMarch 26, 2010
Reviews/decisionsApril 16, 2010
Camera ready versions dueApril 30, 2010
AFM10 WorkshopJuly 14, 2010

Workshop Program

The program includes contributed papers and invited talks selected by the international program committee.

9:00 Invited Talk: System Software Verification Using VCC
Mark Hillebrand
10:00 Break
10:30 Ideas for a high-level proof strategy language
Cliff Jones, Gudmund Grov and Alan Bundy
11:00 Automatic Guidance for Refinement Based Formal Methods
Maria Teresa Llano Rodriguez, Gudmund Grov and Andrew Ireland
11:30 Analyzing Alloy Constraints using an SMT Solver: A Case Study
Aboubakr Achraf El Ghazi and Mana Taghdiri
12:00 Lunch
2:00 Invited Talk: Probabilistic Reasoning with PCE
Sam Owre and N. Shankar
3:00 Break
3:30 Assume-Guarantee for Reachability
Meng Wenrui
4:00 Discussion
5:00 Close of Workshop

Invited Talks

System Software Verification Using VCC
Mark Hillebrand

System software is safety-critical and hard to debug, making it an interesting target for formal verification. Previous system verification efforts have all been based on interactive theorem proving, requiring expert prover knowledge and substantial human effort. In the approach we give here, we use Microsoft's VCC, an automatic verifier for (suitably annotated) concurrent C. We use our approach to fully verify a small hypervisor based on just a few well-defined assumptions.

This work was done in the context of the Verisoft XT project while the author was at the German Research Center for Artificial Intelligence (DFKI GmbH), Saarbruecken, Germany. It was joint work with Eyad Alkassar, Wolfgang Paul, and Elena Petrova from Saarland University, Saarbruecken, Germany.

Probabilistic Reasoning with PCE
Sam Owre and N. Shankar

Markov Logic Networks are a framework for probabilistic inference introduced by Richardson and Domingos. It formalizes a graphical relational model in terms of a first-order logic with probabilities. These models can be used to compute the most probable explanation (MPE) or to compute conditional and marginal probabilities. SRI's Probabilistic Consistency Engine (PCE) is an implementation of the Poon and Domingos MC-SAT method of inference which is based on a Markov Chain Monte Carlo (MCMC) analysis. We demonstrate the capabilities of PCE through some simple examples. We also outline the mathematical background behind this approach to probabilistic inference.

Workshop Organizers

Bruno Dutertre and Hassen Saïdi, SRI International