CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems. Boolean equation systems (Bess) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking and model checking. These problems can be solved on the fly (i.e., without constructing explicitly the state space of the system under analysis) by using a demand-driven construction and resolution of the corresponding Bes. In this article, we present a generic software library dedicated to on-the-fly resolution of alternation-free Bess. Four resolution algorithms are currently provided by the library: algorithms A1 and A2 are general, the latter being optimized to produce small-depth diagnostics, whereas algorithms A3 and A4 are specialized for handling acyclic and disjunctive/conjunctive Bess in a memory-efficient way. The library has been developed within the Cadp verification toolbox using the generic Open/Caesar environment and is currently used for three purposes: on-the-fly equivalence checking modulo five widely used equivalence relations, on-the-fly model checking of regular alternation-free modal μ-calculus, and on-the-fly reduction of state spaces based on τ-confluence .

References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Garavel, Hubert; Lang, Frédéric; Mateescu, Radu: Compositional verification of asynchronous concurrent systems using CADP (2015)
  2. Lang, Frédéric; Mateescu, Radu: Partial model checking using networks of labelled transition systems and Boolean equation systems (2013)
  3. Mateescu, Radu; Serwe, Wendelin: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols (2013) ioport
  4. Gallardo, M. M.; Joubert, C.; Merino, P.; Sanán, D.: A model-extraction approach to verifying concurrent C programs with CADP (2012) ioport
  5. Keiren, Jeroen J. A.; Reniers, Michel A.; Willemse, Tim A. C.: Structural analysis of Boolean equation systems (2012)
  6. Mateescu, Radu; Wijs, Anton: Sequential and distributed on-the-fly computation of weak tau-confluence (2012)
  7. Garavel, Hubert; Lang, Frédéric; Mateescu, Radu; Serwe, Wendelin: CADP 2010: a toolbox for the construction and analysis of distributed processes (2011)
  8. Mateescu, Radu; Monteiro, Pedro T.; Dumas, Estelle; de Jong, Hidde: CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks (2011)
  9. Ploeger, B.; Wesselink, J. W.; Willemse, T. A. C.: Verification of reactive systems via instantiation of parameterised Boolean equation systems (2011)
  10. Alpuente, M.; Feliú, M. A.; Joubert, C.; Villanueva, A.: DATALOG_SOLVE: a Datalog-based demand-driven program analyzer (2009) ioport
  11. Mateescu, Radu; Monteiro, Pedro T.; Dumas, Estelle; de Jong, Hidde: Computation tree regular logic for genetic regulatory networks (2008)
  12. van de Pol, Jaco; Weber, Michael: A multi-core solver for parity games (2008)
  13. Joubert, Christophe; Mateescu, Radu: Distributed on-the-fly model checking and test case generation (2006)
  14. Mateescu, Radu: (CAESAR_SOLVE:) A generic library for on-the-fly resolution of alternation-free Boolean equation systems (2006) ioport