CEGAR

swMATH4605MaRDI QIDQ16776FDOQ16776

Author name not available (Why is that?)

Cited In (37)

• 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
• Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints
• 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
• 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
• 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
• 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