CEGAR

swMATH4605MaRDI QIDQ16776FDOQ16776

Author name not available (Why is that?)

Cited In (37)

• Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification
• Abstraction for Stochastic Systems by Erlang’s Method of Stages
• Minimal counterexamples for linear-time probabilistic verification
• Combining Model Checking and Data-Flow Analysis
• 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
• Effective Verification of Replicated Data Types Using Later Appearance Records (LAR)
• Applying CEGAR to the Petri Net State Equation
• On Abstraction of Probabilistic Systems
• Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains
• Local abstraction refinement for probabilistic timed programs
• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• A game-based abstraction-refinement framework for Markov decision processes
• A Framework for Verification of Software with Time and Probabilities
• 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
• Solving QBF with Counterexample Guided Refinement
• 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
• Compositional Abstraction for Stochastic Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Probabilistic CEGAR
• Infeasible Paths Elimination by Symbolic Execution Techniques
• SMT-Based Bisimulation Minimisation of Markov Models
• Petri nets with name creation for transient secure association
• Variable Probabilistic Abstraction Refinement
• Probabilistic model checking of biological systems with uncertain kinetic rates
• Abstract model repair for probabilistic systems
• Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey
• Refinement and difference for probabilistic automata
• Safety verification for probabilistic hybrid systems

This page was built for software: CEGAR