Treffer: Combined Static and Dynamic Verification of Object Oriented Software Through Partial Proofs

When verifying software one can make use of several verification techniques. These techniques mostly fall in one of two categories: Static Verification and Dynamic Verification. Static verification deals with the analysis of either concrete source code, or a model of it. These kinds of techniques can verify properties over all possible runs of a program. Dynamic verification is 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, e.g., systems with numerous interacting sub-units, concrete (as opposed to abstract) data, etc. On the other hand, its major drawbacks are the impossibility to extrapolate correct observations to all possible runs, and that the monitoring of a property introduces runtime overheads. It is quite clear that static and dynamic verification have largely disjoint strengths. Therefore, their combination can allow the verification process to deal with richer properties, with greater ease. The work presented in this thesis addresses this issue by introducing some manners to combine static and dynamic verification, where partial proofs are used as a means to accomplish the combination. The main novelty in these combinations consists in the fact that all of them consider the use of the partial proofs in the verification process, whereas, in general, other verification approaches discard them right away. The main contributions of this thesis are: (i) ppDATE, an automata-based formalism to specify both data- and control-oriented properties; (ii) structural operational semantics for ppDATE; (iii) a translation of ppDATE to DATE together with a proof of correctness; (iv) StaRVOOrS, a tool for combining (static) deductive verification and runtime verification of object oriented software; (v) a testing focused development methodology which integrates deductive and runtime verification in its workflow; and (vi) a methodology to infer global ...