43 citations · 125 across the 10 of their papers we have counts for
3 papers · 1 filter
Aligator.jl - A Julia Package for Loop Invariant Generation
Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
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. Aligato…
Desingularization of First Order Linear Difference Systems with Rational Function Coefficients
Moulay A. Barkatou, Maximilian Jaroschek
It is well known that for a first order system of linear difference equations with rational function coefficients, a solution that is holomorphic in some left half plane can be ana…
Invariant Generation for Multi-Path Loops with Polynomial Assignments
Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
Program analysis requires the generation of program properties expressing conditions to hold at intermediate program locations. When it comes to programs with loops, these properti…