ZING: SYSTEMATIC STATE SPACE EXPLORATION OF CONCURRENT SOFTWARE

Jakob Rehof
Microsoft Research [Redmond, USA]
http://research.microsoft.com/~rehof

(Lecture notes)

Abstract

Lecture 1:

We give an overview of problems specific to software model checking. We then introduce Zing, a concurrent software model checker that is being developed at Microsoft research. The architecture of Zing and the main innovations and research themes of Zing will be introduced.

Lecture 2:

We describe the Zing input language and give examples of checking models with Zing. We then turn to more specific innovations, focusing on procedure summaries for concurrent programs.

Lecture 3:

We introduce a conformance checker, which has been implemented on top of the Zing engine. We describe the theory of conformance and its implementation in Zing. It is a good example of how the core Zing architecture can be used to build new checking tools. We conclude by reviewing more recent research topics, such as context-bounded model checking and the integration between Zing and a theorem prover for reasoning about symbolic data, including a symbolic heap.

 

Last update February 10, 2006 16:57 EET by local organizers, esscass05_at_cc.ioc.ee
http://cs.ioc.ee/yik/schools/sum2005/

© 2005 Institute of Cybernetics at TUT, All Rights Reserved