
Trace Logic for Inductive Loop Reasoning
We propose trace logic, an instance of manysorted firstorder logic, to...
read it

Subsumption Demodulation in FirstOrder Theorem Proving
Motivated by applications of firstorder theorem proving to software ana...
read it

Layered Clause Selection for Theory Reasoning
Explicit theory axioms are added by a saturationbased theorem prover as...
read it

Interactive Visualization of Saturation Attempts in Vampire
Many applications of formal methods require automated reasoning about sy...
read it

Verifying Relational Properties using Trace Logic
We present a logical framework for the verification of relational proper...
read it

Splitting Proofs for Interpolation
We study interpolant extraction from local firstorder refutations. We p...
read it
Bernhard Gleiss
is this you? claim profile