Cubicle

Cubicle: a parallel smt-based model checker for parameterized systems. Cubicle is a new model checker for verifying safety properties of parameterized systems. It implements a parallel symbolic backward reachability procedure using Satisfiabilty Modulo Theories. Experiments done on classic and challenging mutual exclusion algorithms and cache coherence protocols show that Cubicle is effective and competitive with state-of-the-art model checkers.


References in zbMATH (referenced in 18 articles , 1 standard article )

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

  1. Amat, Nicolas; Berthomieu, Bernard; Dal Zilio, Silvano: On the combination of polyhedral abstraction and SMT-based model checking for Petri nets (2021)
  2. Bozga, Marius; Iosif, Radu; Sifakis, Joseph: Checking deadlock-freedom of parametric component-based systems (2021)
  3. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) (2021)
  4. Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca: Universal invariant checking of parametric systems with quantifier-free SMT reasoning (2021)
  5. Conchon, Sylvain; Delzanno, Giorgio; Ferrando, Angelo: Declarative parameterized verification of distributed protocols via the cubicle model checker (2021)
  6. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: SMT-based verification of data-aware processes: a model-theoretic approach (2020)
  7. Conchon, Sylvain; Declerck, David; Zaïdi, Fatiha: Parameterized model checking on the TSO weak memory model (2020)
  8. Mirzaie, Nahal; Faghih, Fathiyeh; Jacobs, Swen; Bonakdarpour, Borzoo: Parameterized synthesis of self-stabilizing protocols in symmetric networks (2020)
  9. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: Model completeness, covers and superposition (2019)
  10. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: From model completeness to verification of data aware processes (2019)
  11. Peuter, Dennis; Sofronie-Stokkermans, Viorica: On invariant synthesis for parametric systems (2019)
  12. Conchon, Sylvain; Declerck, David; Zaïdi, Fatiha: Cubicle-(\mathcalW): parameterized model checking on weak memory (2018)
  13. Li, Yongjian; Duan, Kaiqiang; Jansen, David N.; Pang, Jun; Zhang, Lijun; Lv, Yi; Cai, Shaowei: An automatic proving approach to parameterized verification (2018)
  14. Roux, Pierre; Iguernlala, Mohamed; Conchon, Sylvain: A non-linear arithmetic procedure for control-command software verification (2018)
  15. Karbyshev, A.; Bjørner, N.; Itzhaky, S.; Rinetzky, N.; Shoham, S.: Property-directed inference of universal invariants or proving their absence (2015)
  16. Li, Yongjian; Pang, Jun; Lv, Yi; Fan, Dongrui; Cao, Shen; Duan, Kaiqiang: ParaVerifier: an automatic framework for proving parameterized cache coherence protocols (2015)
  17. Bertolissi, Clara; Ranise, Silvio: Verification of composed array-based systems with applications to security-aware workflows (2013)
  18. Conchon, Sylvain; Goel, Amit; Krstić, Sava; Mebsout, Alain; Zaïdi, Fatiha: Cubicle: a parallel SMT-based model checker for parameterized systems. Tool paper (2012) ioport