Title: 
-----
A Counter Example Guided Abstraction Refinement Framework for
Compositional Verification of Concurrent C Programs.

Abstract:
--------
Automatic verification of software implementations is a major
challenge in the domain of formal methods. The state of the art
solutions to this problem suffer from one or more of the following
drawbacks. First, most tools attempt to scale to large
implementations. But since they use trace containment as a notion of
conformance, they risk an exponential blowup in the size of the
specification. This potentially prevents them from handling examples
where the specifications are large and complex. Second, there is
little support for compositional reasoning. Third, abstraction
refinement is performed either manually or by considering one counter
example at a time. Multiple counter examples are not used
simultaneously even though this could lead to better refinement
schemes. Finally, counter example guided abstraction refinement is not
integrated smoothly with the handling of concurrency. In this proposal
I present a methodology that attempts to overcome all of these
hurdles. First, exponential blowup due to complex specifications is
avoided by using weak simulation as a notion of conformance. Second,
compositional analysis is allowed for naturally by letting individual
procedures be verified against their respective specifications. Third,
during each abstraction refinement step, multiple counter examples are
used to obtain a minimal set of predicates that suffices to refine the
abstraction. Last, a two-level abstraction refinement scheme achieves
smooth integration of concurrency with counter example guided
abstraction refinement. In conjunction, these techniques are expected
to enable verification of concurrent C programs against complicated
specifications in an automated manner.