5 papers
On the Subspace Orbit Problem and the Simultaneous Skolem Problem
Piotr Bacik, Anton Varonka
The Orbit Problem asks whether the orbit of a point under a matrix reaches a given target set. When the target is a single point, the problem was shown to be decidable in polynomia…
Simple Linear Loops: Algebraic Invariants and Applications
Rida Ait El Manssour, George Kenison, Mahsa Shirmohammadi +1
The automatic generation of loop invariants is a fundamental challenge in software verification. While this task is undecidable in general, it is decidable for certain restricted c…
Determination Problems for Orbit Closures and Matrix Groups
Rida Ait El Manssour, George Kenison, Mahsa Shirmohammadi +2
Computational problems concerning the orbit of a point under the action of a matrix group occur throughout computer science, including in program analysis, complexity theory, quant…
Linear Loop Synthesis for Quadratic Invariants
S. Hitarth, George Kenison, Laura Kovács +1
Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task a…
From Polynomial Invariants to Linear Loops
George Kenison, Laura Kovács, Anton Varonka
Loop invariants are software properties that hold before and after every iteration of a loop. As such, invariants provide inductive arguments that are key in automating the verific…