Talk "A Framework for Static and Runtime Verification of Data- and Control-Oriented Properties"

by Gerardo Schneider

Mon, 09 January 2017 at 04:00 pm in Binz (Rügen), Germany

Joint work with: W. Ahrendt, M. Chimento, G. Pace

Abstract: Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code, are used to verify data-oriented properties, and are able to reason over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques are usually more suitable for control-oriented properties, analysing the current execution of the program in a fully automatic manner. In this talk I will 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 ppDATE enhances the control-oriented property language DATE, supported by the runtime verification tool LARVA, with data-oriented pre/post-conditions, supported by the static verification tool KeY. We have implemented our approach into a verification framework that takes as input a ppDATE specification and a Java program, and perform static and runtime verification as follows: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects.