Aligator.jl - a Julia package for loop invariant generation. 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.
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Bartocci, Ezio; Kovács, Laura; Stankovič, Miroslav: Automatic generation of moment-based invariants for prob-solvable loops (2019)
- Humenberger, Andreas; Jaroschek, Maximilian; Kovács, Laura: Aligator.jl -- a Julia package for loop invariant generation (2018)
- Rabe, Florian (ed.); Farmer, William M. (ed.); Passmore, Grant O. (ed.); Youssef, Abdou (ed.): Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings (2018)