A Calculus for Trace Formula Implication

Specification languages are imperative when trying to verify properties of programs in an automated manner, but they are usually weaker in expressiveness than the programs they are supposed to specify. The state-of-the-art trace formula logic proposed by Hähnle et al. however is a specification language that is at least as expressive as its underlying programs, providing precise specifications of programs with recursion via finite-trace program properties. This logic is presented as a μ-calculus consisting of unary predicates, binary relations, a chop operator handling sequential operations and a fixpoint operator handling program recursion. Hähnle et al. then use a compositional proof calculus in order to establish the proof that a given program satisfies a given trace formula. However, as one of the rules of this calculus needs a trace formula implication oracle as the side condition, reasoning about consequence between trace formulas becomes necessary.

In this thesis, we present a compositional proof calculus for deciding this semantic entailment (i.e. trace inclusion) between trace formulas of a certain shape. Our calculus rules will not only be able to handle unfoldings of recursive fixpoint operations for concrete executions, but also be able to perform fixpoint inductions, thus additionally ensuring derivations of symbolic fixpoint executions. We then extend this base calculus with method contracts and μ-formula synchronization, ensuring applicability of our calculus for even more practical trace inclusion problems.

Whilst we will prove the soundness of our calculus, completeness is not achieved and left for future research, as indicated by various open incompleteness problems. However, as the presented calculus is compositional in nature, extensions with more sophisticated trace inclusion concepts are simple to integrate, thus avoiding conflicts with the already existing proof rule base presented in this thesis.