1 citations · 1 across the 4 of their papers we have counts for
3 papers · 1 filter
NEXP-Completeness and Exponential Coefficient Growth for 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…
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…