A Sequent Calculus For Trace Formula Implication

Abstract

Specification languages are essential in deductive program verification, but they are usually based on first-order logic, hence less expressive than the programs they specify. Recently, trace specification logics with fixed points that are at least as expressive as their target programs were proposed. This makes it possible to specify not merely pre- and postconditions, but the whole trace of even recursive programs. Previous work established a sound and complete calculus to determine whether a program satisfies a given trace formula. However, the applicability of the calculus and prospects for mechanized verification rely on the ability to prove consequence between trace formulas. We present a sound sequent calculus for proving implication (i.e. trace inclusion) between trace formulas. To handle fixed point operations with an unknown recursive bound, fixed point induction rules are used. We also employ contracts and μ-formula synchronization. While this does not yet result in a complete calculus for trace formula implication, it is possible to prove many non-trivial properties.