43 citations · 110 across the 11 of their papers we have counts for
4 papers · 1 filter
Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
Ezio Bartocci, Laura Kovács, Miroslav Stankovič
One of the main challenges in the analysis of probabilistic programs is to compute invariant properties that summarise loop behaviours. Automation of invariant generation is still…
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…
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…