Trace Logic for Inductive Loop Reasoning

Pamina Georgiou, Bernhard Gleiss, Laura Kovács

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 semanti…