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 32 articles )

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

1 2 next

  1. Bartocci, Ezio; Kovács, Laura; Stankovič, Miroslav: Automatic generation of moment-based invariants for prob-solvable loops (2019)
  2. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  3. Chatzieleftheriou, G.; Katsaros, P.: Abstract model repair for probabilistic systems (2018)
  4. Chatterjee, Krishnendu; Chmelík, Martin; Daca, Przemysław: CEGAR for compositional analysis of qualitative properties in Markov decision processes (2015)
  5. Farzan, Azadeh; Kincaid, Zachary; Podelski, Andreas: Proof spaces for unbounded parallelism (2015)
  6. Á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)
  7. Dehnert, Christian; Gebler, Daniel; Volpato, Michele; Jansen, David N.: On abstraction of probabilistic systems (2014)
  8. Delahaye, Benoît; Fahrenberg, Uli; Larsen, Kim G.; Legay, Axel: Refinement and difference for probabilistic automata (2014)
  9. Dräger, Klaus; Kwiatkowska, Marta; Parker, David; Qu, Hongyang: Local abstraction refinement for probabilistic timed programs (2014)
  10. Wimmer, Ralf; Jansen, Nils; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd: Minimal counterexamples for linear-time probabilistic verification (2014)
  11. Dehnert, Christian; Katoen, Joost-Pieter; Parker, David: SMT-based bisimulation minimisation of Markov models (2013)
  12. Rosa-Velardo, Fernando: Petri nets with name creation for transient secure association (2013)
  13. Barbuti, Roberto; Levi, Francesca; Milazzo, Paolo; Scatena, Guido: Probabilistic model checking of biological systems with uncertain kinetic rates (2012)
  14. Ferrer Fioriti, Luis María; Hahn, Ernst Moritz; Hermanns, Holger; Wachter, Björn: Variable probabilistic abstraction refinement (2012)
  15. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
  16. Katoen, Joost-Pieter; van de Pol, Jaco; Stoelinga, Mariëlle; Timmer, Mark: A linear process-algebraic format with data for probabilistic automata (2012)
  17. Kwiatkowska, Marta; Norman, Gethin; Parker, David: Probabilistic verification of Herman’s self-stabilisation algorithm (2012)
  18. Zhang, Lijun; She, Zhikun; Ratschan, Stefan; Hermanns, Holger; Hahn, Ernst Moritz: Safety verification for probabilistic hybrid systems (2012)
  19. Caillaud, Benoît; Delahaye, Benoît; Larsen, Kim G.; Legay, Axel; Pedersen, Mikkel L.; Wąsowski, Andrzej: Constraint Markov chains (2011)
  20. Wimmel, Harro; Wolf, Karsten: Applying CEGAR to the Petri net state equation (2011)

1 2 next