Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
Bit-Precise CHC Satisfiability Using Theory-Modular Reasoning
Omer Rappoport, Orna Grumberg, Yakir Vizel
Deciding satisfiability of Constrained Horn Clauses (CHCs) modulo the theory of fixed-size bit-vectors () is fundamental to bit-precise program verification. However…
cs.LO2024
CTL* Verification and Synthesis using Existential Horn Clauses
Mishel Carelli, Orna Grumberg
This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to specifications, based on translation to E…