|
|
|
TERMINATOR-related presentation materials:
|
Title: Automatically proving program termination
Speaker:
Byron Cook
Place:
CAV'07 Invited talk
Date: July 4 2007
Materials: slides
Abstract:
In this talk I will describe recent research related to automatically
proving program termination.
|
|
Title: Proving thread termination
Speaker:
Byron Cook
Place:
PLDI'07
Date: June 12th 2007
Materials: slides
Abstract:
Concurrent programs are often designed such that certain functions
executing within
critical threads must terminate. Examples of such cases can be
found in
operating systems, web servers, e-mail clients, etc.
Unfortunately,
no known automatic program termination prover supports a
practical
method of proving the termination of threads.
In this paper we describe such a procedure.
The procedure's scalability is achieved through the use of
environment models that
abstract away the surrounding threads.
The procedure's accuracy is due to a novel
method
of incrementally constructing
environment abstractions.
Our method
finds
the conditions that a thread requires of its environment in order to
establish termination
by looking at the
conditions necessary to prove that certain paths through the thread
represent well-founded relations if
executed in isolation of the other threads.
The paper gives a description of
experimental results using an implementation of our procedure
on Windows device drivers, and a
description of a previously unknown bug found with
the tool.
|
|
Title:
Automatically Proving Concurrent Programs Correct
Speaker:
Byron Cook
Place:
Microsoft TechFest'07
Date: March 8th 2007
Materials:
Video
Abstract:
In this talk, I discuss several exciting new developments in the area of automatic tools for proving correctness properties of concurrent programs. This
talk is aimed at a general audience.
|
|
Title:
Variance Analyses from Invariance Analyses
Speaker:
Byron Cook
Place:
Microsoft Research, Redmond
Date: August 8th 2006
Materials:
Video
Abstract:
An invariance assertion for a program location "n" is a formula that always holds at "n" during execution of the program. Program invariance analyses infer invariance assertions that can be useful when trying to prove safety properties. We use the term "variance assertion" to mean a formula that holds between any state at "n" and any previous state that was also at "n". This talk will describe advances in the development of analyses for variance assertions and their application to proving termination and liveness properties. We describe a method of constructing program variance analyses from invariance analyses. If we change the underlying invariance analysis, we get a different variance analysis. We describe several applications of the method, including variance analyses using linear arithmetic and shape analysis. Using experimental results we demonstrate that these variance analyses give rise to a new breed of termination provers which are competitive with and sometimes better than today's state-of-the-art termination provers.
|
|
Title:
Automatically proving the termination of C programs
Speaker:
Byron Cook
Place:
Isaac Newton
Institute for Mathematical Sciences
Date: February 3rd 2006
Materials: slides and audio
Abstract:
In this talk I will discuss Terminator, which is a program termination prover that supports large programs with arbitrarily nested loops or recursive functions, and imperative features such as references, functions with side-effects, and function pointers. Terminator is based on a newly discovered method of counterexample-guided abstraction refinement for program termination proofs. The termination argument is constructed incrementally, based on failed proof attempts. Terminator also infers and proves required program invariants on demand. The lecture will close with information about the results of some experiments with Terminator on Windows device drivers.
|
|
|
 |
|
|
|
