StaRVOOrS : unifying static and runtime verification of Java

Abstract

Over the past decades, several forms of automated verification techniques have been proposed and explored in the literature. These techniques mostly fall in one of two categories: static and dynamic verification. Runtime verification is a dynamic technique concerned with the monitoring of software, providing guarantees that observed runs comply with specified properties. It is strong in analysing systems of a complexity that is difficult to address by static verification, like systems with numerous interacting sub-units, heavy usage of mainstream libraries, real (as opposed to abstract) data, and real world deployments. On the other hand, the major drawbacks of runtime verification are the impossibility to extrapolate correct observations to all possible executions, and that monitoring introduces runtime overheads. In the work we present here, these issues are addressed by combining runtime verification with static verification, such that: (i) Static verification attempts to ‘resolve’ those parts of the properties which can be confirmed statically; (ii) the static results, even if only partial, are used to change the property specification such that generated monitors will not check dynamically what was confirmed statically.