loop synthesis

Determination Problems for Orbit Closures and Matrix Groups

Computational problems concerning the orbit of a point under the action of a matrix group occur in numerous subfields of computer …
R. Ait El Manssour, G. Kenison, M. Shirmohammadi, J. Worrell
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 DOI arXiv
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
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