43 citations · 83 across the 4 of their papers we have counts for
6 papers
Lonely Points in Simplices
Maximilian Jaroschek, Manuel Kauers, Laura Kovacs
Given a lattice L in Z^m and a subset A of R^m, we say that a point in A is lonely if it is not equivalent modulo L to another point of A. We are interested in identifying lonely p…
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…
Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences
Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
Analyzing and reasoning about safety properties of software systems becomes an especially challenging task for programs with complex flow and, in particular, with loops or recursio…
Desingularization Explains Order-Degree Curves for Ore Operators
Shaoshi Chen, Maximilian Jaroschek, Manuel Kauers +1
Desingularization is the problem of finding a left multiple of a given Ore operator in which some factor of the leading coefficient of the original operator is removed. An order-de…