Events

10:00am Jean-Raymond Abrial (ETH Zurich)
Functions and Capabilities of a Theorem Prover to be Used in the Modelling and Implementation of Complex Discrete Systems.In this presentation, I shall describe our experience in designing and using theorem provers for modelling and later implementing complex discrete systems.
First, I shall draw the initial picture by showing the typical proof load (both automatic and interactive) encountered in the development of real projects.
Then, I shall describe the scope and limitations of such a prover and make clear how the working engineer has to interact with it while in the design of a complex system.
Finally, I shall give some indications about the proving techniques we have to use in such a prover.
My final thesis is that such a prover can be put together with a frontend and a backend. The frontend is made of (1) a static checker, (2) a semi-automatic refining tool, and (3) a verification condition generator. The backend is a simple automatic code generator. The result of this association constitutes, in my mind, the “compiler” of tomorrow.
The modelling notation which is to be used as input to this “compiler” is highly mathematically oriented (as TLA+ or Event-B are). These notations are nothing else but the most classical mathematical notations used to describe and refine discrete system models.

J.-R. Abrial is the originator of the Z notation, during his time at the Programming Research Group within the Oxford University Computing Laboratory, and later the B-Method, two leading formal methods for software engineering. He is the author of The B-Book: Assigning Programs to Meanings. For much of his career he has been an independent consultant, as much at home working with industry as academia. Currently he is a Professor at ETH Zurich in Switzerland.

11:15am Leslie Lamport (MSR Mountain View)
TLA, TLA+, and Proofs

This talk will introduce the logic TLA, explain the rationale for the specification language TLA+ based on TLA, and discuss the implications for a TLA+ theorem prover.

Leslie Lamport studied mathematics at M.I.T., from which he obtained a B.S. degree in 1960, and at Brandeis University, where he was awarded an M.A. degree in 1963 and a Ph.D. degree in 1972.
Dr. Lamport taught mathematics at Marlboro College from 1965 to 1969. He worked at Massachusetts Computer Associates from 1970 to 1977, at SRI International from 1977 to 1985, and at the Digital (later Compaq) Systems Research Center from 1985 to 2001. Since 2001, he has been a senior researcher at Microsoft Research’s Silicon Valley laboratory.
Dr. Lamport’s research has been centered on concurrency and fault-tolerance. He is the inventor of several well-known concurrent and distributed algorithms, including early algorithms for tolerating “Byzantine” faults. He did seminal work on the theory of cache coherence and distributed systems. He has also developed methods for formally specifying and verifying concurrent systems.
Dr. Lamport received the Principles of Distributed Computing conference’s influential paper award in 2000, and the Dijkstra Prize in 2005. He is a member of the National Academy of Engineering, and has received honorary degrees from the University of Rennes, Christian Albrechts University in Kiel, the EPFL in Lausanne, and the University of Lugano.

12:30am Damien Doligez (INRIA Rocquencourt)
Extensibility of a FOL prover

I will present a theorem that only Zenon can prove, and use it as an example to demonstrate the most interesting feature of tableau-based provers, that they are easily extended to handle particular classes of theorems.

Damien Doligez is a researcher in project Gallium at INRIA. He is one of the implementers of Objective Caml, and the author of the Zenon theorem prover.