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…