Trace Logic for Inductive Loop Reasoning

TL;DR

This paper introduces trace logic, a first-order logic framework for automating partial correctness proofs of programs with loops, leveraging inductive invariants and integrated into the RAPID reasoning system.

Contribution

It presents trace logic as a novel formalism for loop reasoning, extending program semantics and automating inductive proofs within the RAPID framework.

Findings

Successfully proved correctness of programs involving linear integer arithmetic.

Extended RAPID with trace logic and superposition reasoning.

Demonstrated automation of inductive loop reasoning.

Abstract

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.