6 papers
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…
iSMC: A BDD-based Symbolic Model Checker with Interactive Certification
Philipp Czerner, Javier Esparza, Konrad Winslow
We present iSMC, the first self-certifying model checker with interactive certification, a certification paradigm based on the theory of interactive proof systems. iSMC is a symbol…
Undecidability of the Emptiness Problem for Weak Models of Distributed Computing
Flavio T. Principato, Javier Esparza, Philipp Czerner
Esparza and Reiter have recently conducted a systematic comparative study of weak asynchronous models of distributed computing, in which a network of identical finite-state machine…
The Expressive Power of Uniform Population Protocols with Logarithmic Space
Philipp Czerner, Vincent Fischer, Roland Guttenberg
Population protocols are a model of computation in which indistinguishable mobile agents interact in pairs to decide a property of their initial configuration. Originally introduce…
Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
Michael Blondin, Michaël Cadilhac, Xin-Yi Cui +3
Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checkin…
The Black Ninjas and the Sniper: On Robustness of Population Protocols
Benno Lossin, Philipp Czerner, Javier Esparza +2
Population protocols are a model of distributed computation in which an arbitrary number of indistinguishable finite-state agents interact in pairs to decide some property of their…