3 citations · 6 across the 8 of their papers we have counts for
12 papers
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 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…
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 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…
Computing Inductive Invariants of Regular Abstraction Frameworks
Philipp Czerner, Javier Esparza, Valentin Krasotin +1
Regular transition systems (RTS) are a popular formalism for modeling infinite-state systems in general, and parameterised systems in particular. In a CONCUR 22 paper, Esparza et a…
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…
Making Practical: Efficient Interactive Protocols for BDD Algorithms
Eszter Couillard, Philipp Czerner, Javier Esparza +1
We show that interactive protocols between a prover and a verifier, a well-known tool of complexity theory, can be used in practice to certify the correctness of automated reasonin…
Breaking through the -space barrier: Population Protocols Decide Double-exponential Thresholds
Philipp Czerner
Population protocols are a model of distributed computation in which finite-state agents interact randomly in pairs. A protocol decides for any initial configuration whether it sat…
Fast and Succinct Population Protocols for Presburger Arithmetic
Philipp Czerner, Roland Guttenberg, Martin Helfrich +1
In their 2006 seminal paper in Distributed Computing, Angluin et al. present a construction that, given any Presburger predicate as input, outputs a leaderless population protocol…
Decision Power of Weak Asynchronous Models of Distributed Computing
Philipp Czerner, Roland Guttenberg, Martin Helfrich +1
Esparza and Reiter have recently conducted a systematic comparative study of models of distributed computing consisting of a network of identical finite-state automata that coopera…
Lower Bounds on the State Complexity of Population Protocols
Philipp Czerner, Javier Esparza, Jérôme Leroux
Population protocols are a model of computation in which an arbitrary number of indistinguishable finite-state agents interact in pairs. The goal of the agents is to decide by stab…