# Trace Logic for Inductive Loop Reasoning

arXiv: https://arxiv.org/abs/2008.01387 · HTML: https://mlsanity.com/paper/2008.01387/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Aug 2020.

## Built on by (most cited first, 1 of 1)

- [Data-driven Verification of Procedural Programs with Integer Arrays](https://mlsanity.com/paper/2505.15958/) (2025)

## Abstract (arXiv)

We propose trace logic, an instance of many-sorted first-order logic, to automate the partial correctness verification of programs containing loops. Trace logic generalizes semantics of program locations and captures loop semantics by encoding properties at arbitrary timepoints and loop iterations. We guide and automate inductive loop reasoning in trace logic by using generic trace lemmas capturing inductive loop invariants. Our work is implemented in the RAPID framework, by extending and integrating superposition-based first-order reasoning within RAPID. We successfully used RAPID to prove correctness of many programs whose functional behavior are best summarized in the first-order theories of linear integer arithmetic, arrays and inductive data types.