Papers for

program analyzers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Injective transition graphs simplify checking cyclic proof termination

Global Trace Condition for Injective Transition Graphs

Abstract: We formulate the global trace condition, GTC, for cyclic proofs as a particular case of the size-change termination condition, or SCT. We express cyclic proofs through a variant of size-change graphs, called transition graphs, whose edges are labelled by (finite) bipartite relations. We show that injective transition graphs suffice to encode cyclic pre-proofs for a variant of Brotherston and Simpson's sequent calculus with inductive definitions. The injectivity of transition graphs corresponds to restricting SCT to fan-in-free graphs. Then we prove that an essentially weaker condition implies SCT in this case, and hence GTC.

Tue 3 NovLogic in Computer Science
The gist
Ensuring that certain logical proofs stop and don’t loop forever is important in computer science. The authors describe a new way to represent these proofs using special graphs called injective transition graphs. They show that checking a simpler condition on these graphs is enough to guarantee the proofs will terminate, which can make verification easier. This connects ideas from proof theory and program termination analysis.
Open → 2611.04788v1