43 citations · 170 across the 19 of their papers we have counts for
13 papers · 1 filter
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…
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…
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…
Subsumption Demodulation in First-Order Theorem Proving
Bernhard Gleiss, Laura Kovacs, Jakob Rath
Motivated by applications of first-order theorem proving to software analysis, we introduce a new inference rule, called subsumption demodulation, to improve support for reasoning…
Interactive Visualization of Saturation Attempts in Vampire
Bernhard Gleiss, Laura Kovacs, Lena Schnedlitz
Many applications of formal methods require automated reasoning about system properties, such as system safety and security. To improve the performance of automated reasoning engin…
Verifying Relational Properties using Trace Logic
Gilles Barthe, Renate Eilers, Pamina Georgiou +3
We present a logical framework for the verification of relational properties in imperative programs. Our work is motivated by relational properties which come from security applica…
Splitting Proofs for Interpolation
Bernhard Gleiss, Laura Kovacs, Martin Suda
We study interpolant extraction from local first-order refutations. We present a new theoretical perspective on interpolation based on clearly separating the condition on logical s…
Coming to Terms with Quantified Reasoning
Laura Kovacs, Simon Robillard, Andrei Voronkov
The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essentia…
The Vampire and the FOOL
Evgenii Kotelnikov, Laura Kovács, Giles Reger +1
This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arr…
A First Class Boolean Sort in First-Order Theorem Proving and TPTP
Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
To support reasoning about properties of programs operating with boolean values one needs theorem provers to be able to natively deal with the boolean sort. This way, program prope…