Sciweavers

Share
TYPES
1998
Springer

Metatheory of Verification Calculi in LEGO - To what Extent Does Syntax Matter?

12 years 2 months ago
Metatheory of Verification Calculi in LEGO - To what Extent Does Syntax Matter?
Investigating soundness and completeness of verification calculi for imperative programming languages is a challenging task. Incorrect results have been published in the past. We take advantage of the computer-aided proof tool LEGO to interactively establish soundnessand completenessof both Hoare Logic and the operation decomposition rules of the Vienna Development Method with respect to operational semantics. We deal with parameterless recursive procedures and local variables in the context of total correctness. In this paper, we discuss in detail the role of representations for expressions, assertions and verification calculi. To what extent is syntax relevant? One needs to carefully select an appropriate level of detail in the formalisation in order to achieve one's objectives.
Thomas Kleymann
Added 06 Aug 2010
Updated 06 Aug 2010
Type Conference
Year 1998
Where TYPES
Authors Thomas Kleymann
Comments (0)
books