Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Verification Constraint Problems with Strengthening
verfasst von : Aaron R. Bradley, Zohar Manna
Erschienen in: Theoretical Aspects of Computing - ICTAC 2006
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The deductive method reduces verification of safety properties of programs to, first, proposing inductive assertions and, second, proving the validity of the resulting set of first-order verification conditions. We discuss the transition from
verification conditions
to
verification constraints
that occurs when the deductive method is applied to parameterized assertions instead of fixed expressions (
e.g.
,
p
0
+
p
1
j
+
p
2
k
≥0, for parameters
p
0
,
p
1
, and
p
2
, instead of 3 +
j
–
k
≥0) in order to discover inductive assertions. We then introduce two new verification constraint forms that enable the incremental and property-directed construction of inductive assertions. We describe an iterative method for solving the resulting constraint problems. The main advantage of this approach is that it uses off-the-shelf constraint solvers and thus directly benefits from progress in constraint solving.