Keynote speakers

Tom Ball (Principal Researcher, Microsoft Research, Redmond)

Title: Towards scalable modular checking of user-defined properties

Home page: http://research.microsoft.com/~tball/

Abstract: Theorem-prover based modular checkers have the potential to perform scalable and fairly precise checking of user-defined properties by combining precise intraprocedural reasoning with user-defined procedure abstractions. However, such tools have seldom been deployed on large software applications of industrial relevance due to the annotation burden required to provide the procedure abstractions. We present a case study of applying a modular checker HAVOC to check properties about the synchronization protocol of a core Microsoft Windows component with more than 300,000 lines of code and 1500 procedures. The effort found 45 serious bugs in the component with modest annotation effort and low false alarms; most of these bugs have since been fixed by the developers of the module. We describe our experience in using a modular checker to create various property checkers for finding errors in a well-tested application of this scale, and our design decisions to find them with low false alarms, modest annotation burden and high coverage. We also describe preliminary user experience in using the tool for checking security related properties in several Windows components in a product group.

More information about HAVOC is available at http://research.microsoft.com/havoc/

Joint work with Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer and Julien Vanegue

Gerwin Klein (National ICT Australia)

Title: The L4.verified Project

Home page: http://www.cse.unsw.edu.au/~kleing/

Abstract: Last year, the NICTA L4.verifed project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security.

Matthew Parkinson (Microsoft Research, Cambridge)

Title: The Next 700 Separation Logics

Home page: http://www.cl.cam.ac.uk/~mjp41/

Abstract: In recent years, separation logic has brought great advances in the world of verification.  However, there is a disturbing trend for each new library or concurrency primitive to require a new separation logic.  In this extended abstract, I will argue that we shouldn't be inventing new separation logics, but should find the right logic to reason about interference, and have a powerful abstraction mechanism to enable the library's implementation details to be correctly abstracted.  Adding new concurrency libraries should simply be a matter of verification, not of new logics.