TL;DR
Aligator.jl is an open-source Julia package that automatically generates polynomial invariants for extended P-solvable loops with nested conditionals, aiding program verification and analysis.
Contribution
It introduces a novel method combining symbolic computation and algebraic techniques to automatically derive polynomial invariants for complex loops.
Findings
Successfully generates polynomial invariants for extended P-solvable loops.
Utilizes Gr"obner basis computation for variable elimination.
Implemented as an open-source Julia package.
Abstract
We describe the Aligator.jl software package for automatically generating all polynomial invariants of the rich class of extended P-solvable loops with nested conditionals. Aligator.jl is written in the programming language Julia and is open-source. Aligator.jl transforms program loops into a system of algebraic recurrences and implements techniques from symbolic computation to solve recurrences, derive closed form solutions of loop variables and infer the ideal of polynomial invariants by variable elimination based on Gr\"obner basis computation.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
