CEGAR

Counterexample-guided abstraction refinement (CEGAR) has been en vogue for the automatic verification of very large systems in the past years. When trying to apply CEGAR to the verification of probabilistic systems, various foundational questions arise. This paper explores them in the context of predicate abstraction


References in zbMATH (referenced in 31 articles )

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

1 2 next

  1. Chatzieleftheriou, G.; Katsaros, P.: Abstract model repair for probabilistic systems (2018)
  2. Mordan, Vitaly; Mutilin, Vadim: Checking several requirements at once by CEGAR (2016)
  3. Chatterjee, Krishnendu; Chmelík, Martin; Daca, Przemysław: CEGAR for compositional analysis of qualitative properties in Markov decision processes (2015)
  4. Farzan, Azadeh; Kincaid, Zachary; Podelski, Andreas: Proof spaces for unbounded parallelism (2015)
  5. Ábrahám, Erika; Becker, Bernd; Dehnert, Christian; Jansen, Nils; Katoen, Joost-Pieter; Wimmer, Ralf: Counterexample generation for discrete-time Markov models: an introductory survey (2014)
  6. Dehnert, Christian; Gebler, Daniel; Volpato, Michele; Jansen, David N.: On abstraction of probabilistic systems (2014)
  7. Delahaye, Beno^ıt; Fahrenberg, Uli; Larsen, Kim G.; Legay, Axel: Refinement and difference for probabilistic automata (2014)
  8. Dräger, Klaus; Kwiatkowska, Marta; Parker, David; Qu, Hongyang: Local abstraction refinement for probabilistic timed programs (2014)
  9. Wimmer, Ralf; Jansen, Nils; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd: Minimal counterexamples for linear-time probabilistic verification (2014)
  10. Dehnert, Christian; Katoen, Joost-Pieter; Parker, David: SMT-based bisimulation minimisation of Markov models (2013)
  11. Rosa-Velardo, Fernando: Petri nets with name creation for transient secure association (2013)
  12. Barbuti, Roberto; Levi, Francesca; Milazzo, Paolo; Scatena, Guido: Probabilistic model checking of biological systems with uncertain kinetic rates (2012)
  13. Ferrer Fioriti, Luis María; Hahn, Ernst Moritz; Hermanns, Holger; Wachter, Björn: Variable probabilistic abstraction refinement (2012)
  14. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
  15. Katoen, Joost-Pieter; van de Pol, Jaco; Stoelinga, Mariëlle; Timmer, Mark: A linear process-algebraic format with data for probabilistic automata (2012)
  16. Kwiatkowska, Marta; Norman, Gethin; Parker, David: Probabilistic verification of Herman’s self-stabilisation algorithm (2012)
  17. Zhang, Lijun; She, Zhikun; Ratschan, Stefan; Hermanns, Holger; Hahn, Ernst Moritz: Safety verification for probabilistic hybrid systems (2012)
  18. Caillaud, Beno{^ı}t; Delahaye, Beno{^ı}t; Larsen, Kim G.; Legay, Axel; Pedersen, Mikkel L.; Wąsowski, Andrzej: Constraint Markov chains (2011)
  19. Wimmel, Harro; Wolf, Karsten: Applying CEGAR to the Petri net state equation (2011)
  20. Abdulla, Parosh Aziz; Chen, Yu-Fang; Delzanno, Giorgio; Haziza, Frédéric; Hong, Chih-Duo; Rezine, Ahmed: Constrained monotonic abstraction: a CEGAR for parameterized verification (2010)

1 2 next