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öbner basis computation.
CITATION STYLE
Humenberger, A., Jaroschek, M., & Kovács, L. (2018). Aligator.jl – A julia package for loop invariant generation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11006 LNAI, pp. 111–117). Springer Verlag. https://doi.org/10.1007/978-3-319-96812-4_10
Mendeley helps you to discover research relevant for your work.