StaRVOOrS: Combined Static and Runtime Verification of Object-Oriented Software
Wolfgang Ahrendt
Chalmers University
SWS Colloquium
Wolfgang Ahrendt is associate professor at Chalmers University of Technology in Gothenburg, Sweden. His major interests are software verification, theorem proving, and runtime verification. He one of the people behind the KeY approach and system, and has recently co-edited the book 'Deductive Software Verification - The KeY Book' (LNCS 100001).
Static verification techniques are used to analyse and prove properties about programs before they are deployed. In particular, deductive
verification techniques often work directly on the source code and are used to verify data-oriented properties of all possible executions. In
contrast, runtime verification techniques have been extensively used for control-oriented properties, and analyse concrete executions that
occur in the deployed program. I present an approach in which data-oriented and control-oriented properties may be stated in a single formalism
amenable to both static and dynamic verification techniques. The specification language enhances a control-oriented property language
with data-oriented pre/postconditions. We show how such specifications can be analysed using a combination of the deductive verification system
KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY performs fully automated proof attempts, the resulting
partial proofs are analysed, and used to optimize the specification for efficient runtime checking.