Senior Research Engineer, NICTA
Research Fellow, Australian National University, Australia
Director, Institut fuer Softwaretechnik und Programmiersprachen, Uni Luebec, Germany
The Theory and Practice of SALT - Structured Assertion Language for Temporal Logic
Project website: SALT
SALT is a general purpose specification and assertion language developed for creating concise temporal specifications to be used in industrial verification environments. It incorporates ideas of existing approaches, such as PSL or Dwyer's specification patterns, in that it provides operators to express scopes and exceptions, as well as support for a subset of the regular expressions. On the one hand side, SALT exceeds specific features of these approaches, for example, in that it allows the nesting of scopes and supports the specification of real-time properties. On the other hand, SALT is fully translatable to LTL, if no real-time operators are used, and to TLTL (also known as state-clock logic), if real-time operators appear in a specification. The latter is needed in particular for verification tasks to do with reactive systems imposing strict execution times and dead-lines. SALT's semantics is defined in terms of a translation to temporal (real-time) logic, and a compiler is freely available from the project web site, including an interactive web interface to test drive the compiler. In this tutorial, we will detail on the theoretical foundations of SALT as well as its practical use in applications such as model checking and runtime verification.
Katholieke Universiteit Leuven, Belgium
VeriFast: a Powerful, Sound, Predictable, Fast Verifier for C and Java
Project website: VeriFast
VeriFast is a verifier for single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic. To enable rich specifications, the programmer may define inductive datatypes, primitive recursive pure functions over these datatypes, and abstract separation logic predicates. To enable verification of these rich specifications, the programmer may write lemma functions, i.e., functions that serve only as proofs that their precondition implies their postcondition. The verifier checks that lemma functions terminate and do not have side-effects. Verification proceeds by symbolic execution, where the heap is represented as a separation logic formula. Since neither VeriFast itself nor the underlying SMT solver do any significant search, verification time is predictable and low. We are currently using VeriFast to verify fine-grained concurrent data structures, unloadable kernel modules, and JavaCard programs.
Microsoft Research, USA
Verification of Functional Correctness of Concurrent C Programs with VCC
Project website: VCC
VCC is an industrial-strength verification environment for low-level concurrent systems code written in C. VCC takes a program (annotated with function contracts, state assertions, and type invariants) and attempts to prove the correctness of these annotations. VCC's verification methodology allows global two-state invariants that restrict update of shared state and enforces simple, semantic conditions sufficient for checking those global invariants modularly. VCC works by translating C, via the Boogie intermediate verification language, to verification conditions handled by the Z3 SMT solver. The environment includes tools for monitoring proof attempts and constructing partial counterexample executions for failed proofs and has been used to verify functional correctness of tens of thousands of lines of Microsoft's Hyper-V virtualization platform and of SYSGO's embedded real-time operating system PikeOS.