VSTTE on Tuesday, August 22nd

Session 1 (09:00‑10:30)

09:00‑10:00

Sumit Gulwani (Microsoft Research) Program Verification using Probabilistic Techniques [ppt]

10:00‑10:30

Kevin Elphinstone (NICTA/UNSW) Gerwin Klein (NICTA) Rafal Kolanski (NICTA/UNSW) Formalising a High-Performance Microkernel This paper argues that a pragmatic approach is needed for integrating design and formalisation of complex systems. We report on our approach to designing the seL4 operating system microkernel API and its formalisation in Isabelle/HOL. The formalisation consists of the systematic translation of significant parts of the functional programming language Haskell into Isabelle/HOL, including monad-based code. We give an account of the experience, decisions and outcomes in this translation as well as the technical problems we encountered together with our solutions. The longer-term goal is to demonstrate that formalisation and verification of a large, complex, OS-level code base is feasible with current tools and methods and is in the order of magnitude of traditional development cost.

Break (10:30‑11:00)

Session 2 (11:00‑12:30)

11:00‑11:30	Oystein Thorsen (Michigan Technological University) Charles Wallace (Michigan Technological University) Automated Verification of UPC Consistency The UPC programming language is a shared memory extension to ANSI C. Its memory consistency model is relaxed, allowing for a high degree of optimization, but also permitting behavior which may be surprising to the naive programmer. To allow better understanding of this memory model, we present a tool for analyzing the behavior of UPC programs. Given an execution trace, the tool determines whether the results are compatible with the UPC memory model. The tool is targeted at newcomers to UPC who want to learn about its memory model and at developers who want to verify possible behaviors of their programs.
11:30‑12:00	Jonathan Ostroff (Department of Computer Science and Eng., York University) Chen-wei Wang (York University) Eric Kerfoot (Computing Laboratory, University of Oxford) Faraz Ahmadi Torshizi (Computer Science and Eng., York University, Toronto) Automated Model-based Verification of Object-Oriented Code ESpec is a suite of tools that facilitates the testing and verification of Eiffel programs in an integrated environment. The suit includes unit testing tools and Fit tables (for customer requirements) that report contract failures. This paper describes ES-Verify (part of ESpec) for automatically verifying a significant subset of Eiffel constructs written with a value semantics. The tool includes a mathematical model library (sequences, sets, bags and maps) for writing high level specifications, and a translator that converts the Eiffel code into the language used by the Perfect Developer (PD) theorem prover. Preliminary experience indicates that the vast majority of verification conditions are quickly and automatically discharged, including loop variants and invariants. ES-Verify is the first automated Eiffel verification tool (to our knowledge) and allows the developer to use the clean syntax and object-oriented structures of Eiffel, together with its mature industrial strength design by contract mechanism.
12:00‑12:30	Patrice Chalin (Concordia University) Perry James (Concordia University) Cross-Verification of JML Tools: An ESC/Java2 Case Study This paper presents a case study in the use of the JML Run-time Assertion Checker (RAC) compiler on ESC/Java2, an extended static checker for the Java Modeling Language (JML). We believe that overall product quality is maximized by the use of complementary verification tools. Use of the JML RAC allowed us to uncover deeper problems with the design of ESC/Java2 than was possible with static analysis alone. Some problems that were found with the RAC are discussed, along with tentative and implemented solutions.

Lunch break (12:30‑14:00)

Session 3 (14:00‑15:30)

14:00‑14:30

Eric Feron (Georgia Institute of Technology) Arnaud Venet (Kestrel Technology) Static Stability Analysis of embedded, autocoded software This paper describes a research program aimed at verifying safety properties of embedded, autocoded software, as it interacts in closed loop with a physical artifact. The paper describes how the combination of two powerful techniques, abstract interpretation and control systems theory, can yield novel static analyzers to verify that the functional properties of the system specifications carry over to their software implementation, accounting for the many additional structures and discretizations present in the software implementation.

14:30‑15:30

Jim Grundy (Intel Strategic Cad Laboratories) Challenges and Lessons for Software Verification [pdf]

Break (15:30‑16:00)

Session 4 (16:00‑17:00)

16:00‑17:00

Discussion