Loop Synthesis

Linear Loop Synthesis for Quadratic Invariants
Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. …
S. Hitarth, G. Kenison, L. Kovács, A. Varonka
PDF Cite DOI arXiv
(Un)Solvable Loop Analysis
Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler …
D. Amrollahi, E. Bartocci, G. Kenison, L. Kovács, M. Moosbrugger, M. Stankovič
Cite arXiv
From Polynomial Invariants to Linear Loops
Loop invariants are software properties that hold before and after every iteration of a loop. As such, invariants provide inductive …
G. Kenison, L. Kovács, A. Varonka
PDF Cite DOI arXiv