KIT | KIT-Bibliothek | Impressum | Datenschutz
Open Access Logo
URN: urn:nbn:de:swb:90-41244

An improved rule for while loops in deductive program verification

Beckert, Bernhard; Schlager, Steffen; Schmitt, Peter H.


The performance and usability of deductive program verification
systems can be greatly enhanced if specifications of programs
and program parts not only consist of the usual
pre-/post-condition pairs and invariants but also include
additional information on which memory locations are changed by
executing a program. This allows to separate the aspects of (a)
which locations change and (b) how they change, state the change
information in a compact way, and make the proof process more
efficient. In this paper, we extend this idea from method
specifications to loop invariants; and we define a proof rule
for while loops that makes use of the change information
associated with the loop body. It has been implemented and is
successfully used in the KeY software verification system.

Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Forschungsbericht
Jahr 2005
Sprache Englisch
Identifikator ISSN: 1432-7864

KITopen-ID: 1000004124
Verlag Karlsruhe
Serie Interner Bericht. Fakultät für Informatik, Universität Karlsruhe ; 2005,26
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page