43 citations · 110 across the 11 of their papers we have counts for
18 papers
Automating Induction by Reflection
Johannes Schoisswohl, Laura Kovács
Despite recent advances in automating theorem proving in full first-order theories, inductive reasoning still poses a serious challenge to state-of-the-art theorem provers. The rea…
Automating Induction by Reflection
Johannes Schoisswohl, Laura Kovacs
Despite recent advances in automating theorem proving in full first-order theories, inductive reasoning still poses a serious challenge to state-of-the-art theorem provers. The rea…
Summing Up Smart Transitions
Neta Elad, Sophie Rain, Neil Immerman +2
Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transa…
MORA -- Automatic Generation of Moment-Based Invariants
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic
We introduce MORA, an automated tool for generating invariants of probabilistic programs. Inputs to MORA are so-called Prob-solvable loops, that is probabilistic programs with poly…
Formalizing Graph Trail Properties in Isabelle/HOL
Laura Kovacs, Hanna Lachnitt, Stefan Szeider
We describe a dataset expressing and proving properties of graph trails, using Isabelle/HOL. We formalize the reasoning about strictly increasing and decreasing trails, using weigh…
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…