29 citations · 37 across the 8 of their papers we have counts for
Showing 2020Show all
2 papers · 1 filter
cs.LO2020★ 5 cited
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…
cs.PL2020
Algebra-based Loop Synthesis
Andreas Humenberger, Laura Kovács
We present an algorithm for synthesizing program loops satisfying a given polynomial loop invariant. The class of loops we consider can be modeled by a system of algebraic recurren…