43 citations · 93 across the 5 of their papers we have counts for
6 papers
Algebra-Based Reasoning for Loop Synthesis
Andreas Humenberger, Daneshvar Amrollahi, Nikolaj Bjørner +1
Provably correct software is one of the key challenges of our software-driven society. Program synthesis -- the task of constructing a program satisfying a given specification -- i…
Algebra-based Synthesis of Loops and their Invariants (Invited Paper)
Andreas Humenberger, Laura Kovacs
Provably correct software is one of the key challenges in our softwaredriven society. While formal verification establishes the correctness of a given program, the result of progra…
Algebra-based Loop Synthesis
Andreas Humenberger, Laura Kovács
We present an algorithm for synthesizing program loops satisfying a given polynomial loop invariant. The class of loops we consider can be modeled by a system of algebraic recurren…
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…
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…