2026· International Conference on Theory and Applications of Satisfiability Testing· pp. 17:1-17:19· 0 citations· 36 references
Computer Science
TL;DR
PalRUP is introduced – an LRUP -based proof format and a bottleneck-free, decentralized parallel checking procedure that only uses the (parallel) file system and is composed of a set of small, sequential trusted components.
FLEX is presented, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions.
J. Khan, Petros Markopoulos, Nicolás Lehmann et al.· 0 citations
This work introduces a framework that addresses both verification levels in the Lean theorem prover, and can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families.
This system description reports on how Kissat’s award-winning techniques were adapted to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition, to support efficient linear proof production with hints.
Florian Pollitt, Mathias Fleury, Katalin Fazekas et al.· 0 citations
