43 citations · 125 across the 10 of their papers we have counts for
10 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…
Improved Polynomial Remainder Sequences for Ore Polynomials
Maximilian Jaroschek
Polynomial remainder sequences contain the intermediate results of the Euclidean algorithm when applied to (non-)commutative polynomials. The running time of the algorithm is depen…
Adapting Real Quantifier Elimination Methods for Conflict Set Computation
Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine
The satisfiability problem in real closed fields is decidable. In the context of satisfiability modulo theories, the problem restricted to conjunctive sets of literals, that is, se…
Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings
Moulay A. Barkatou, Maximilian Jaroschek, Suzy S. Maddah
In this paper, we present an algorithm for computing a fundamental matrix of formal solutions of completely integrable Pfaffian systems with normal crossings in several variables.…
Ore Polynomials in Sage
Manuel Kauers, Maximilian Jaroschek, Fredrik Johansson
We present a Sage implementation of Ore algebras. The main features for the most common instances include basic arithmetic and actions; gcrd and lclm; D-finite closure properties;…
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…