2 papers
cs.LO2026
A Resolution-Based Interactive Proof System for UNSAT
Philipp Czerner, Javier Esparza, Valentin Krasotin +1
Modern SAT or QBF solvers are expected to produce correctness certificates. However, certificates have worst-case exponential size (unless NP=coNP), and at recent SAT competitions…
cs.FL2025
Regular Model Checking for Systems with Effectively Regular Reachability Relation
Javier Esparza, Valentin Krasotin
Regular model checking is a well-established technique for the verification of regular transition systems (RTS): transition systems whose initial configurations and transition rela…