swMATH4605MaRDI QIDQ16776FDOQ16776
Author name not available (Why is that?)
Official website: http://rw4.cs.uni-sb.de/~bwachter/cav08.html
Cited In (62)
- Solving QBF with counterexample guided refinement
- Abstraction for Stochastic Systems by Erlang’s Method of Stages
- A framework for verification of software with time and probabilities
- Minimal counterexamples for linear-time probabilistic verification
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Counting minimal unsatisfiable subsets
- 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
- Local abstraction refinement for probabilistic timed programs
- Counterexample generation for discrete-time Markov models: an introductory survey
- A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
- Compositional abstraction for stochastic systems
- Farkas certificates and minimal witnesses for probabilistic reachability constraints
- Applying CEGAR to the Petri net state equation
- A game-based abstraction-refinement framework for Markov decision processes
- 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
- CEGAR for compositional analysis of qualitative properties in Markov decision processes
- Algorithms for computing minimal unsatisfiable subsets of constraints
- SIGREF
- PASS
- COMICS
- Cseq
- DiPro
- PARAM
- Orion
- Pinapa
- SCOOT
- AMUSE
- MUP
- SatAbs
- Lazy-CSeq
- BEACON
- Storm
- monabs
- SACO
- Ultimate Kojak
- CPAlien
- FrankenBit
- Jakstab
- MU-CSeq
- Aligator.jl
- Symbiotic 2
- Reveal: A Formal Verification Tool for Verilog Designs
- Verification and refutation of probabilistic specifications via games
- A linear process-algebraic format with data for probabilistic automata
- Constrained monotonic abstraction: a CEGAR for parameterized verification
- Tools and Algorithms for the Construction and Analysis of Systems
- Probabilistic CEGAR
- Petri nets with name creation for transient secure association
- PRINSYS
- 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
