[Prev][Next][Index][Thread]

Region-Based Model Abstraction (paper announcement)

We are pleased to announce the paper:

Region-Based Model Abstraction.

By Jeremy Condit, James R. Larus, Sriram K. Rajamani and Jakob Rehof.
Microsoft Research technical report MSR-TR-2003-47.

This paper is available from the MSR technical report series and from

http://www.research.microsoft.com/~rehof/publications.html#region


The abstract follows.

ABSTRACT:
We present a new technique for abstracting programs to models suitable
for
state space exploration (e.g., using a model checker).  This abstraction
technique is based on a region type system in which regions are
interpreted as sets of values.  A major benefit of the region
abstraction
is that it soundly supports aggressive state space reduction and state
size reduction in the presence of aliasing without relying on either
imprecise global static alias analysis or a large pointer slice of the
source program prior to model construction.

Region types themselves contain only locally sound alias information;
however, our models are globally sound by computing dynamically with
region names at model checking time. This technique effectively shifts
part of the alias analysis to the model checker and leads to state space
reduction as well as enhanced model precision.  Region types also
provide
a flexible framework for adjusting the tradeoff between model precision
and performance.  We have used these techniques to implement a
region-based model compiler for C#.



Comments and/or questions are very welcome!

Best regards

--Jakob