19 citations · 20 across the 5 of their papers we have counts for
6 papers
NEXP-Completeness of Existential Presburger Arithmetic with Divisibility
Ignacio Barros, Michaël Cadilhac, Guillermo A. Pérez
We prove that satisfiability for existential Presburger arithmetic with divisibility (EPAD) is NEXP-hard. Together with the known NEXP upper bound, this establishes NEXP-completene…
Population Protocols over Ordered Agents
Michael Blondin, Michaël Cadilhac, Benjamin Courchesne +3
Population protocols are a distributed computation model in which a collection of anonymous, finite-state agents interact in randomly chosen pairs and update their states according…
Knee-Deep in C-RASP: A Transformer Depth Hierarchy
Andy Yang, Michaël Cadilhac, David Chiang
It has been observed that transformers with greater depth (that is, more layers) have more capabilities, but can we establish formally which capabilities are gained? We answer this…
Data Structures for Finite Downsets of Natural Vectors: Theory and Practice
Michaël Cadilhac, Vanessa Flügel, Guillermo A. Pérez +1
Manipulating downward-closed sets of vectors forms the basis of so-called antichain-based algorithms in verification. In that context, the dimension of the vectors is intimately ti…
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 Reactive Synthesis Competition (SYNTCOMP): 2018-2021
Swen Jacobs, Guillermo A. Perez, Remco Abraham +22
We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Th…