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