CEGAR
From MaRDI portal
Cited in
(65)- Solving QBF with counterexample guided refinement
- Minimal counterexamples for linear-time probabilistic verification
- Abstraction for Stochastic Systems by Erlang’s Method of Stages
- A framework for verification of software with time and probabilities
- Counting minimal unsatisfiable subsets
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Proof spaces for unbounded parallelism
- Probabilistic verification of Herman's self-stabilisation algorithm
- Constraint Markov chains
- Variable probabilistic abstraction refinement
- On Abstraction of Probabilistic Systems
- PRINSYS
- Local abstraction refinement for probabilistic timed programs
- A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
- Counterexample generation for discrete-time Markov models: an introductory survey
- Compositional abstraction for stochastic systems
- Farkas certificates and minimal witnesses for probabilistic reachability constraints
- A game-based abstraction-refinement framework for Markov decision processes
- Applying CEGAR to the Petri net state equation
- SMT-based bisimulation minimisation of Markov models
- Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
- Automated verification and synthesis of stochastic hybrid systems: a survey
- SIGREF
- PRISM
- LiQuor
- MRMC
- PASS
- COMICS
- Cseq
- DiPro
- PARAM
- Orion
- Pinapa
- SCOOT
- AMUSE
- MUP
- SatAbs
- Lazy-CSeq
- BEACON
- Storm
- CEGAR for compositional analysis of qualitative properties in Markov decision processes
- monabs
- SACO
- Ultimate Kojak
- CPAlien
- FrankenBit
- Jakstab
- MU-CSeq
- Aligator.jl
- Symbiotic 2
- Algorithms for computing minimal unsatisfiable subsets of constraints
- A linear process-algebraic format with data for probabilistic automata
- Verification and refutation of probabilistic specifications via games
- Reveal: A Formal Verification Tool for Verilog Designs
- Constrained monotonic abstraction: a CEGAR for parameterized verification
- Probabilistic CEGAR
- Tools and Algorithms for the Construction and Analysis of Systems
- Petri nets with name creation for transient secure association
- Combining model checking and data-flow analysis
- Effective verification of replicated data types using later appearance records (LAR)
- Time-bounded model checking of infinite-state continuous-time Markov chains
- Probabilistic model checking of biological systems with uncertain kinetic rates
- Abstract model repair for probabilistic systems
- Refinement and difference for probabilistic automata
- Safety verification for probabilistic hybrid systems
This page was built for software: CEGAR
