Reuse in Software Verification by Abstract Method Calls^*

Reiner Hähnle¹, Ina Schaefer², and Richard Bubel¹

¹Department of Computer Science, Technische Universität Darmstadt, Germany
haehnle@cs.tu-darmstadt.de
bubel@cs.tu-darmstadt.de

²Institute for Software Engineering, Technische Universität Braunschweig, Germany
i.schaefer@tu-braunschweig.de

Abstract. A major obstacle facing adoption of formal software verification is the difficulty to track changes in the target code and to accomodate them in specifications and in verification arguments. We introduce abstract method calls, a new verification rule for method calls that can be used in most contract-based verification settings. By combining abstract method calls, structured reuse in specification contracts, and caching of verification conditions, it is possible to detect reusability of contracts automatically via first-order reasoning. This is the basis for a verification framework that is able to deal with code undergoing frequent changes.

^*Partly funded by the EU project FP7-231620 HATS (http://www.hats-project.eu) and by the German Science Foundation (SCHA1635/2-1)

LNAI 7898, p. 300 ff.

Full article in PDF | BibTeX

lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013