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

Showing results 1 to 20 of 34.
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. Aissat, Romain; Voisin, Frédéric; Wolff, Burkhart: Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths (2016)
  5. Chatterjee, Krishnendu; Chmelík, Martin; Daca, Przemysław: CEGAR for compositional analysis of qualitative properties in Markov decision processes (2015)
  6. Farzan, Azadeh; Kincaid, Zachary; Podelski, Andreas: Proof spaces for unbounded parallelism (2015)
  7. Mukund, Madhavan; Gautham Shenoy, R.; Suresh, S. P.: Effective verification of replicated data types using later appearance records (LAR) (2015)
  8. Á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)
  9. Dehnert, Christian; Gebler, Daniel; Volpato, Michele; Jansen, David N.: On abstraction of probabilistic systems (2014)
  10. Delahaye, Benoît; Fahrenberg, Uli; Larsen, Kim G.; Legay, Axel: Refinement and difference for probabilistic automata (2014)
  11. Dräger, Klaus; Kwiatkowska, Marta; Parker, David; Qu, Hongyang: Local abstraction refinement for probabilistic timed programs (2014)
  12. Wimmer, Ralf; Jansen, Nils; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd: Minimal counterexamples for linear-time probabilistic verification (2014)
  13. Dehnert, Christian; Katoen, Joost-Pieter; Parker, David: SMT-based bisimulation minimisation of Markov models (2013)
  14. Rosa-Velardo, Fernando: Petri nets with name creation for transient secure association (2013)
  15. Barbuti, Roberto; Levi, Francesca; Milazzo, Paolo; Scatena, Guido: Probabilistic model checking of biological systems with uncertain kinetic rates (2012)
  16. Ferrer Fioriti, Luis María; Hahn, Ernst Moritz; Hermanns, Holger; Wachter, Björn: Variable probabilistic abstraction refinement (2012)
  17. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
  18. Katoen, Joost-Pieter; van de Pol, Jaco; Stoelinga, Mariëlle; Timmer, Mark: A linear process-algebraic format with data for probabilistic automata (2012)
  19. Kwiatkowska, Marta; Norman, Gethin; Parker, David: Probabilistic verification of Herman’s self-stabilisation algorithm (2012)
  20. Zhang, Lijun; She, Zhikun; Ratschan, Stefan; Hermanns, Holger; Hahn, Ernst Moritz: Safety verification for probabilistic hybrid systems (2012)

1 2 next