Constructing and Reasoning about Abstractions and Refinements
Project members:
Shiva Nejati, Arie Gurfinkel, Marsha Chechik
Description
Most realistic artifacts are too large to verify directly and
need to be abstracted. Such abstractions should be constructed
so that verification of the abstracted system allows us to say something
about correctness of the original system.
Classical abstraction is sound only with respect to universallyquantified
properties, e.g., if an invariant holds on an abstract system, it holds
on the concrete one. If a reachability property holds on an
abstract system, it is not clear whether it holds on the original one.
If a universallyquantified property fails to hold, one can use
counterexample based abstraction refinement to make
the abstraction more precise so as to avoid the spurious counterexample.
3valued abstraction preserves truth and falsity of arbitrary temporal logic
properties. Of course, it is possible that the verification engine
determines that the answer to the property is Maybe, at which point
the verification is inconclusive and the abstraction needs to be
refined.
There are many ways to compute 3valued abstractions. One of them
comes from abstract interpretation of programs, where a predicate p
is determined to be True if it is true in the concretization of the
system, False if it is false in the concretization, and Maybe if
its value in the concrete system cannot be determined.
Current and Future Projects in This Area
 Abstract interpretation. Our previous work, reported
in ISF and in Wei Ding's M.Sc. thesis, has started our interest in
multivalued modeling and reasoning, but a lot more work needs
to be done here. Looking for students.
 3Valued SPIN. SPIN is a stateoftheart modelchecker.
Our goal is to create a version of SPIN that can analyze threevalued
models. The work on this project has started, and is related to
finitepath semantics for LTL and many other projects we do.
 Stuttering Refinement. Over the past year, Shiva Nejati
has been working on a type of refinement for
threevalued models that allows one abstract state to be repeated
(a finite number of times) and preserves a large class of temporal
logic properties. Shiva also has an algorithm for determining
whether two models are stutter refinements of each other.
This work is her M.Sc. thesis, and a paper written in collaboration
with Arie Gurfinkel and myself is currently being finished.
 3valued CounterExample Based Abstraction Refinement
The idea here is to build a framework using counterexamples for
those properties that resulted in Maybe answers to refine abstractions.
We are also interested in comparing this framework with the classical
in order to quantify effectiveness of 3valued abstraction. Looking
for students to join Arie Gurfinkel and myself on this project.
 From Classical to 3valued AbstractionOne can reduce 3valued modelchecking to two questions to
the classical modelchecker. This should allow reuse of a lot of
ideas associated with reasoning about classical abstractions,
in particular, assume/guarantee reasoning. We are interested
in investigating such parallels and looking for students to join in.
 We are also very interested in case studies that use 3valued
abstractions.
Most relevant publications and related work:
Classical abstraction and refinement
 Clarke, Grumberg, Jha, Lu, Veith.
Counterexampleguided
abstraction refinement. In Proceedings of CAV'00.
 There are several excellent surveys and talks on this area:
 Orna Grumberg, Abstractions and Reductions in Model Checking,
In NATO Science Series, Vol. 62, 2001, Marktoberdorf summer school.
 David Schmidt. Proving
Properties about Abstractions and Refinements, Bell Labs, Naperville,
IL, Feb. 2000 (it is a talk)
 David Schmidt [Talk].
Binary
relations for abstraction and refinement (17 November). Technical
Report 20003. Corrected version of the paper in Proc. Workshop on Refinement
and Abstraction, Amagasaaki, Japan, Nov. 1999, Elsevier Electronic
Notes in Theoretical Computer Science
 Yannis Kassios's presentation of some of these
results as part of a
course project in csc 2108
 D. Dams, R. Gerth, O. Grumberg, Abstract Interpretation of Reactive Systems,
ACM Transactions on Programming Languages and Systems (TOPLAS), 1997.
3valued Abstraction and Refinement
 M. Chechik, W. Ding, Lightweight Reasoning about Program Correctness,
Information Systems Frontiers, 2002.
 S. Shoham, O. Grumberg. A GameBased Framework for CTL CounterExamples and 3Valued AbstractionRefinement, CAV'03.
 Shiva Nejati, Refinement Relations on Partial Specifications,
M.Sc. thesis, University of Toronto, 2003.
 P. Godefroid, R. Jagadeesan, Automatic Abstraction Using Generalized
Model Checking, in CAV'02
Classical and 3valued modelchecking

M. Chechik, B. Devereux, A. Gurfinkel. ModelChecking Infinite StateSpace Systems with FineGrained Abstractions Using SPIN, in SPIN'01 Workshop on
ModelChecking Software.
 G.J. Holzmann, "The Model Checker SPIN", IEEE Transactions on Software
Engineering, 279295, Vol. 23, No. 5, May 1997
 G. Bruns, P. Godefroid, Model Checking Partial State Spaces with 3Valued Temporal Logics, CAV'99.
 G. Bruns, P. Godefroid, Generalized Model Checking: Reasoning about
Partial State Spaces, CONCUR'00.
Last updated: Sept. 3, 2003