In this project we investigate solutions of
three fundamental problems hindering the
application of finite-state verification (``model checking'')
techniques to software:
-
the derivation
of sound, finite-state models for distributed software systems
-
the automation of the finite-model construction technique
-
the limitation of the cardinality
of the constructed models to a tractable size
We attack these problems by employing new technology based on the
maturing formal-methods techniques of
abstract interpretation and partial evaluation:
-
Abstract interpretation, a technique for symbolically executing
programs, will be employed to define a hierarchy of semantically correct
``property sets'' that can be used with symbolic execution. Crucially,
the result of a
symbolic execution with abstract interpretation is a
finite-state model that
is a safe abstraction of the state space of the original program.
-
Partial evaluation, an automated program simplification/transformation
methodology, will be used as the ``engine'' to drive the abstract
interpretation. Partial evaluation
provides the needed automation,
because it is general purpose and robust---it can
be applied to any abstract interpretation and any source program,
and it will generate automatically the desired finite-state models.
-
Finally, the interaction of abstract interpretation and partial
evaluation generates a synergy otherwise absent---the cardinality of
the automatically generated finite-state models can be
controlled by tuning partial evaluation's specialization
and inlining algorithms to interact optimally with the
choice of property sets within the abstract interpretation.
Our methodology liberates the software designer from the burden of
designing by hand ad-hoc, potentially incorrect, abstract models of
software systems. It also allows the separation-of-concerns of
model creation from model checking, meaning that the
optimal model checker can be selected for checking a specific class
of models.
In addition, the robustness of partial evaluation technology allows it to
be applied to modular or ``open'' programs, advancing the frontier of
compositional model checking.
We also envisage that our integration of abstract interpretation and
partial evaluation machinery will let us undertake serious
application of radical state-space reduction techniques based on
semantically pseudo-safe abstractions, where symbolic execution
undertaken by abstract interpretation might be semantically unsound for
some program properties, but it is semantically sound for
the correctness properties of interest to the software designer.
