A Sequent Calculus For Trace Formula Implication
Niklas Heidler, Reiner Hähnle
TL;DR
The paper tackles the problem of proving implication (trace inclusion) between trace formulas that capture the behavior of imperative programs with recursive procedures. It develops a sound sequent calculus for trace formula consequence, enabling reasoning about traces via judgments of the form $S{:}Φ$ and using fixed-point induction, contracts, and μ-synchronization to handle unbounded recursion. While complete completeness remains out of reach, the authors provide a robust core calculus plus extensions that prove many non-trivial properties and pave the way for mechanization. This approach strengthens modular verification by linking program semantics to trace formulas and offers practical means to verify recursive programs through trace-based specifications.
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.