Aligator swMATH ID: 29 Software Authors: Kovács, Laura Description: We describe the new software package Aligator for automatically inferring polynomial loop invariants. The package combines algorithms from symbolic summation and polynomial algebra with computational logic, and is applicable to the rich class of P-solvable loops. Aligator contains routines for checking the P-solvability of loops, transforming them into a system of recurrence equations, solving recurrences and deriving closed forms of loop variables, computing the ideal of polynomial invariants by variable elimination, invariant filtering and completeness check of the resulting set of invariants. Homepage: http://mtc.epfl.ch/software-tools/Aligator/ Related Software: Mathematica; fastZeil; hyper; Dependencies; z3; TPTP; RISCErgoSum; E Theorem Prover; JAMPACK; iProver; JAMA; VAMPIRE; Orbital library; RSOLVER; REDLOG; KeYmaera; QEPCAD; CSDP; Abella; LogAnswer Cited in: 10 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Aligator: A Mathematica package for invariant generation. (System description). Zbl 1165.68525Kovács, Laura 2008 all top 5 Cited by 13 Authors 8 Kovács, Laura Ildikó 2 Humenberger, Andreas 2 Jaroschek, Maximilian 1 Armando, Alessandro 1 Baumgartner, Peter 1 Dowek, Gilles 1 Henzinger, Thomas A. 1 Hottelier, Thibaud 1 Kovacs, Adalbert 1 Platzer, André 1 Quesel, Jan-David 1 Rümmer, Philipp 1 Voronkov, Andrei Cited in 1 Serial 1 Lecture Notes in Computer Science all top 5 Cited in 7 Fields 10 Computer science (68-XX) 1 General and overarching topics; collections (00-XX) 1 Combinatorics (05-XX) 1 Field theory and polynomials (12-XX) 1 Commutative algebra (13-XX) 1 Algebraic geometry (14-XX) 1 Numerical analysis (65-XX) Citations by Year