Lectures

Verification of concurrency and transactions

Speaker: C.A.R. Hoare , Microsoft Research, Cambridge, England

Further reading:  

• Fine-grain concurrency
• Compensable transactions

Automated Formal Methods with PVS, SAL, and Yices

Speaker: Natarajan Shankar, SRI International Computer Science Laboratory

Description:
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.

Lectures:
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

Short biography:
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

Description:
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 will cover:

• 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

Short biography:
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.

Talks

Title: SPARK - a high-integrity programming language and its verification environment

Friday 14th September - 16:45 - 19:00 hs

Speaker: Dr Roderick Chapman, Praxis High Integrity Systems Limited, England

Abstract:
SPARK is a programming language and set of verification tools designed for the development of high-integrity applications. SPARK was designed with verifiability as the primary 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 soley static verification, using design-by-contract, information flow analysis, verificaton-condition 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, and some examples of industrial SPARK projects in aerospace, rail and government security. Finally, the presentation will cover some of the challenging aspects of the implementation, including the design of the contract language, state abstraction, dealing with volatile I/O devices, and interfacing to other languages.

Short biography:
Rod Chapman is a principal engineer with Praxis High Integrity Systems. Rod has been involved with the design of both safety- and security-critical 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.