Showing cs.LOShow all
2 papers · 1 filter
cs.LO2025
The Vampire Diary
Filip Bártek, Ahmed Bhayat, Robin Coutelier +10
During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now…
cs.LO2024
PolySAT: Word-level Bit-vector Reasoning in Z3
Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann +2
PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-d…