Verification of concurrency and transactions
Speaker: C.A.R. Hoare , Microsoft Research, Cambridge, England
Automated Formal Methods with PVS, SAL, and Yices
Speaker: Natarajan Shankar, SRI International Computer Science Laboratory
Verification relies crucially on modeling and specification languages as
well as automated deduction technology. We examine a suite of languages and
deduction tools implemented in systems such as PVS (Prototype Verification
System) , SAL (Symbolic Analysis Laboratory), and the Yices SMT solver. The
capabilities in these tools include expressive type systems, powerful type
checking, interactive proof construction, combination decision procedures,
Boolean simplification, rewriting, symbolic model checking, bounded model
checking, predicate abstraction, test generation, efficient code generation,
and symbolic simulation. The course is intended as an introduction to the
effective use of these verification systems as well as a tutorial on
constructing deductive tools.
Lecture 1: An Overview of Logic
Lectures 2 & 3: Specification and Proof with PVS
Lectures 4 & 5: Modeling Transition Systems and Model Checking with SAL
Lecture 6: Constraint Solving with Yices
Shankar is a researcher at the SRI International Computer Science
Laboratory, and a co-developer of several of the tools and techniques
covered in the course. He has a Ph.D. in Computer Science from the
University of Texas at Austin, and is the author of "Metamathematics,
Machines, and Goedel's Proof" published by Cambridge University Press.
Developing provably correct software with Spec# and Boogie
Speaker: Peter Müller, Microsoft Research
Spec# is an extension of the object-oriented language C#. It extends
the type system to include non-null types and provides method
contracts as well as object invariants. Boogie is a static program
verifier for Spec# programs based on an automatic theorem prover.
This set of lectures will use Spec# and Boogie to introduce the key
concepts for the verification of object-oriented programs. The lecures
- the Spec# language and its type system
- the architecture of the verification system
- the generation of verification conditions
- the Boogie methodology for the verification of object invariants
- data abstraction using model fields and pure methods
- a verification methodology for concurrent Spec# programs
Peter Müller is a Researcher in the Programming Languages and Methods Group at Microsoft
Research, Redmond. Previously he was Assistant Professor and head of the Software Component
Technology Group at the Computer Science Department of ETH Zurich. His work focuses on formal
specification and verification of object-oriented software.
Title: SPARK - a high-integrity programming language and its verification
Friday 14th September - 16:45 - 19:00 hs
Speaker: Dr Roderick Chapman, Praxis High Integrity Systems Limited, England
SPARK is a programming language and set of verification tools designed
for the development of
high-integrity applications. SPARK was designed with verifiability as
design goal - this leads to some unusual trade-offs in the design, which
set it apart
from other contemporary languages. The verification tools also focus on
verification, using design-by-contract, information flow analysis,
generation and theorem proving. This presentation will cover the design
goals of SPARK,
its major features, the various forms of analysis provided by the tools,
examples of industrial SPARK projects in aerospace, rail and government
Finally, the presentation will cover some of the challenging aspects of
implementation, including the design of the contract language, state
dealing with volatile I/O devices, and interfacing to other languages.
Rod Chapman is a principal engineer with Praxis High Integrity Systems.
Rod has been involved with the design of both safety- and
software with Praxis for many years, including significant contributions
to many of
Praxis' key-note projects such as SHOLIS, MULTOS CA, Tokeneer, and the
development of the SPARK language and verification tools.
He is a chartered engineer and a Fellow of the BCS.