AFM on Wednesday, July 14th

09:00‑10:00 Invited Talk
Location: IF 4.31+4.33
09:00 Mark Hillebrand
System Software Verification Using VCC

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.

10:30‑12:00 Session 1
Location: IF 4.31+4.33
10:30 Cliff Jones, Gudmund Grov and Alan Bundy
Ideas for a high-level proof strategy language
11:00 Maria Teresa Llano Rodriguez, Gudmund Grov and Andrew Ireland
Automatic Guidance for Refinement Based Formal Methods
11:30 Aboubakr Achraf El Ghazi and Mana Taghdiri
Analyzing Alloy Constraints using an SMT Solver: A Case Study
14:00‑15:00 Invited Talk
Location: IF 4.31+4.33
14:00 Sam Owre and N. Shankar
Probabilistic Reasoning with PCE

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.

15:30‑17:00 Session 2
Location: IF 4.31+4.33
15:30 Meng Wenrui
Assume-Guarantee for Reachability
16:00 Discussion