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.
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).
| Position papers due | March 26, 2010 |
| Reviews/decisions | April 16, 2010 |
| Camera ready versions due | April 30, 2010 |
| AFM10 Workshop | July 14, 2010 |
The program includes contributed papers and invited talks selected by the international program committee.
| 9:00 | Invited Talk: System Software Verification
Using VCC |
| 10:00 | Break |
| 10:30 | Ideas for a high-level proof strategy
language |
| 11:00 | Automatic Guidance for Refinement Based Formal
Methods |
| 11:30 | Analyzing Alloy Constraints using an SMT Solver: A
Case Study |
| 12:00 | Lunch |
| 2:00 | Invited Talk: Probabilistic Reasoning with PCE |
| 3:00 | Break |
| 3:30 | Assume-Guarantee for Reachability |
| 4:00 | Discussion |
| 5:00 | Close of Workshop |
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.
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.