5 citations · 9 across the 3 of their papers we have counts for
6 papers
Trace Logic for Inductive Loop Reasoning
Pamina Georgiou, Bernhard Gleiss, Laura Kovács
We propose trace logic, an instance of many-sorted first-order logic, to automate the partial correctness verification of programs containing loops. Trace logic generalizes semanti…
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…
Layered Clause Selection for Theory Reasoning
Bernhard Gleiss, Martin Suda
Explicit theory axioms are added by a saturation-based theorem prover as one of the techniques for supporting theory reasoning. While simple and effective, adding theory axioms can…
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…