Counterexample-guided abstraction refinement for symbolic model checking
From MaRDI portal
Publication:3452508
DOI10.1145/876638.876643zbMath1325.68145OpenAlexW2127574686WikidataQ124822574 ScholiaQ124822574MaRDI QIDQ3452508
Yuan Lu, Orna Grumberg, Helmut Veith, Somesh Jha, Edmund M. Clarke
Publication date: 12 November 2015
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/876638.876643
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Related Items (only showing first 100 items - show all)
Configurable verification of timed automata with discrete variables ⋮ Quantified maximum satisfiability ⋮ Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving ⋮ DKL: an efficient algorithm for learning deterministic Kripke structures ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Software Verification with PDR: An Implementation of the State of the Art ⋮ Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ How testing helps to diagnose proof failures ⋮ Code obfuscation against abstraction refinement attacks ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Lattice-based refinement in bounded model checking ⋮ An abstraction-refinement methodology for reasoning about network games ⋮ Recognition of Nested Gates in CNF Formulas ⋮ Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances ⋮ SAT-Based Model Checking ⋮ Abstraction and Abstraction Refinement ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Transfer of Model Checking to Industrial Practice ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Controller/Orchestrator Synthesis via Filtration ⋮ Diagnosability of fair transition systems ⋮ An iterative approach to precondition inference using constrained Horn clauses ⋮ Reusing predicate precision in value analysis ⋮ Automated circular assume-guarantee reasoning ⋮ On using data abstractions for model checking refinements ⋮ Online minimization of sensor activation for supervisory control ⋮ New Search Strategies for the Petri Net CEGAR Approach ⋮ Lower Bound Techniques for QBF Proof Systems ⋮ Branching-time logics with path relativisation ⋮ Minimal counterexamples for linear-time probabilistic verification ⋮ A model building framework for answer set programming with external computations ⋮ Compositional abstraction refinement for control synthesis ⋮ Synchronous counting and computational algorithm design ⋮ A canonical form based decision procedure and model checking approach for propositional projection temporal logic ⋮ Specifying graph languages with type graphs ⋮ A proof system for unified temporal logic ⋮ Preface of the special issue in memoriam Helmut Veith ⋮ 3-Valued Circuit SAT for STE with Automatic Refinement ⋮ \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms ⋮ Change-of-bases abstractions for non-linear hybrid systems ⋮ Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms ⋮ A View from the Engine Room: Computational Support for Symbolic Model Checking ⋮ A unifying view on SMT-based software verification ⋮ First-order \(\mu\)-calculus over generic transition systems and applications to the situation calculus ⋮ Consistency and refinement for interval Markov chains ⋮ Efficient strategies for CEGAR-based model checking ⋮ Fixed point guided abstraction refinement for alternating automata ⋮ When does abstraction help? ⋮ Test generation from event system abstractions to cover their states and transitions ⋮ Three optimizations for assume-guarantee reasoning with \(L^{*}\) ⋮ Lazy Abstraction-Based Controller Synthesis ⋮ Boosting Lazy Abstraction for SystemC with Partial Order Reduction ⋮ Complexity-sensitive decision procedures for abstract argumentation ⋮ Certifying inexpressibility ⋮ Syntax-guided synthesis for lemma generation in hardware model checking ⋮ Towards Parallel Boolean Functional Synthesis ⋮ Verification of Boolean programs with unbounded thread creation ⋮ Abstraction-Based Algorithm for 2QBF ⋮ Acceptance in incomplete argumentation frameworks ⋮ Propositional proof systems based on maximum satisfiability ⋮ An automatic abstraction technique for verifying featured, parameterised systems ⋮ Horn clause verification with convex polyhedral abstraction and tree automata-based refinement ⋮ Inference of ranking functions for proving temporal properties by abstract interpretation ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ An abstraction-refinement framework for trigger querying ⋮ Correctness kernels of abstract interpretations ⋮ Underapproximation for model-checking based on universal circuits ⋮ Paraconsistent computation tree logic ⋮ Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey ⋮ Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Incompleteness of states w.r.t. traces in model checking ⋮ Generating models of infinite-state communication protocols using regular inference with abstraction ⋮ Tutorial on Model Checking: Modelling and Verification in Computer Science ⋮ Compositional reasoning for shared-variable concurrent programs ⋮ A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability ⋮ Fifty years of Hoare's logic ⋮ Language-Based Abstraction Refinement for Hybrid System Verification ⋮ Omission-Based Abstraction for Answer Set Programs ⋮ A novel approach to verifying context free properties of programs ⋮ Refinement-Based CFG Reconstruction from Unstructured Programs ⋮ SAT-Based Model Checking without Unrolling ⋮ Automata Learning with Automated Alphabet Abstraction Refinement ⋮ Weakening additivity in adjoining closures ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ TAGED Approximations for Temporal Properties Model-Checking ⋮ Fixpoint Guided Abstraction Refinement for Alternating Automata ⋮ A framework for analysing state-abstraction methods ⋮ A Configurable CEGAR Framework with Interpolation-Based Refinements ⋮ Game-theoretic simulation checking tool ⋮ Pakota: A System for Enforcement in Abstract Argumentation ⋮ Local proofs for global safety properties ⋮ Falsification-aware semantics and sequent calculi for classical logic ⋮ A semantic framework for the abstract model checking of tccp programs ⋮ Distributing the Workload in a Lazy Theorem-Prover ⋮ Online Relaxation Refinement for Satisficing Planning: On Partial Delete Relaxation, Complete Hill-Climbing, and Novelty Pruning ⋮ Solving QBF with counterexample guided refinement ⋮ Abstraction-based incremental inductive coverability for Petri nets
This page was built for publication: Counterexample-guided abstraction refinement for symbolic model checking
