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).

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

AG Audience

English

90 Minutes

Saarbrücken

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.

Annika Meiser

0681 9303 9105

--email hidden

Yes

Kaiserslautern

G26

111

passcode not visible

logged in users only