Counterexample-guided abstraction refinement
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- A theory of structural stationarity in the \(\pi\)-calculus
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Integration of verification methods for program systems
- Lattice-based refinement in bounded model checking
- Preface of the special issue in memoriam Helmut Veith
- On relative and probabilistic finite counterability
- Experience of improving the BLAST static verification tool
- Safe \& robust reachability analysis of hybrid systems
- A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability
- Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
- Solving finite-linear-path CTL-formulas using the CEGAR approach
- Improving neural network verification through spurious region guided refinement
- Using state abstractions to compute personalized contrastive explanations for AI agent behavior
- Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving
- Faster pushdown reachability analysis with applications in network verification
- Property-directed verification and robustness certification of recurrent neural networks
- Satisfiability and synthesis modulo oracles
- Abstraction based verification of stability of polyhedral switched systems
- Extracting counterexamples induced by safety violation in linear hybrid systems
- Learning inductive invariants by sampling from frequency distributions
- Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol
- Analysis of correct synchronization of operating system components
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- Unbounded procedure summaries from bounded environments
- Loop summarization using state and transition invariants
- Correctness kernels of abstract interpretations
- Counter-example guided program verification
- Partial predicate abstraction and counter-example guided refinement
- NIL: learning nonlinear interpolants
- Automated planning as an early verification tool for distributed control
- An approximation framework for solvers and decision procedures
- A layered algorithm for quantifier elimination from linear modular constraints
- Counterexample-guided predicate abstraction of hybrid systems
- Verification of SpecC using predicate abstraction
- GSTE is partitioned model checking
- System-level state equality detection for the formal dynamic verification of legacy distributed applications
- Consistency-preserving refactoring of refinement structures in Event-B models
- Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
- Verifying a scheduling protocol of safety-critical systems
- Counterexample-guided abstraction refinement for symmetric concurrent programs
- An automatic method for the dynamic construction of abstractions of states of a formal model
- Verification of Boolean programs with unbounded thread creation
- Combining search space partition and abstraction for LTL model checking
- Incompleteness of states w.r.t. traces in model checking
- Compositional SCC analysis for language emptiness
- A semantic framework for the abstract model checking of tccp programs
- A framework for compositional verification of multi-valued systems via abstraction-refinement
- A program analysis framework for \textit{tccp} based on abstract interpretation
- Lazy slicing for state-space exploration
- Predicate diagrams for the verification of real-time systems
- When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
- A complete refinement procedure for regular separability of context-free languages
- An abstraction algorithm for the verification of generalized C-slow designs
- Relaxed stratification: a new approach to practical complete predicate refinement
- Counter abstraction in the CSP/FDR setting
- View-augmented abstractions
- A three-value abstraction technique for the verification of epistemic properties in multi-agent systems
- Predicate abstraction for dense real-time systems
- Verification of random graph transformation systems
- Automated formal analysis and verification: an overview
- Whale: an interpolation-based algorithm for inter-procedural verification
- Lazy synthesis
- Quantitative abstraction refinement
- On Abstraction of Probabilistic Systems
- Incremental SAT-based method with native Boolean cardinality handling for the Hamiltonian cycle problem
- A counterexample-guided abstraction-refinement framework for Markov decision processes
- Counterexample validation and interpolation-based refinement for forest automata
- Automatic data-abstraction in model checking multi-agent systems
- Projecting transition systems: overcoming state explosion in concurrent system verification
- Abstraction-based algorithm for 2QBF
- An assume guarantee approach for checking quantified array assertions
- Satisfiability solving and model generation for quantified first-order logic formulas
- Distributed and predictable software model checking
- Sound and complete abstract graph transformation
- Predicate abstraction for program verification
- Verification of Hybrid Systems
- Temporal logic verification for delay differential equations
- Model Checking MSVL Programs Based on Dynamic Symbolic Execution
- Counterexample-Guided Refinement of Template Polyhedra
- Effect-polymorphic behaviour inference for deadlock checking
- LCTD: test-guided proofs for C programs on LLVM
- Abstraction Refinement for Quantified Array Assertions
- Refinement of Trace Abstraction
- Abstract Interpretation from a Topological Perspective
- Counterexample-guided abstraction refinement for symbolic model checking
- Bonsai: cutting models down to size
- Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction
- The Birth of Model Checking
- Automated Assume-Guarantee Reasoning by Abstraction Refinement
- Probabilistic CEGAR
- Abstraction for model checking multi-agent systems
- A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement
- Constrained monotonic abstraction: a CEGAR for parameterized verification
- Example-guided abstraction simplification
- Abstract Counterexample-Based Refinement for Powerset Domains
- Predicate Abstraction in a Program Logic Calculus
- Dynamic Path Reduction for Software Model Checking
- Fixpoint-Guided Abstraction Refinements
- Verifying Reference Counting Implementations
- Abstraction refinement with Craig interpolation and symbolic pushdown systems
This page was built for publication: Counterexample-guided abstraction refinement
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2754081)
