SAT-Based Model Checking (Q3176368): Difference between revisions

@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-319-10575-8_10
+Normal rank
@@ Property / OpenAlex ID @@
+W2803222079
@@ Property / OpenAlex ID: W2803222079 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2729082
@@ Property / cites work: Q2729082 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Methods in Computer-Aided Design
@@ Property / cites work: Formal Methods in Computer-Aided Design / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q2848677
@@ Property / cites work: Q2848677 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q2769592
@@ Property / cites work: Q2769592 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2753756
@@ Property / cites work: Q2753756 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / rank @@
+Normal rank
@@ Property / cites work @@
+Satisfiability Modulo Theories
@@ Property / cites work: Satisfiability Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Symbolic Counter Abstraction for Concurrent Software
+Normal rank
@@ Property / cites work @@
+Context-aware counter abstraction
@@ Property / cites work: Context-aware counter abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804893
@@ Property / cites work: Q4804893 / rank @@
+Normal rank
@@ Property / cites work @@
+Invariant Synthesis for Combined Theories
@@ Property / cites work: Invariant Synthesis for Combined Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Linear Encodings of Bounded LTL Model Checking
@@ Property / cites work: Linear Encodings of Bounded LTL Model Checking / rank @@
+Normal rank
@@ Property / cites work @@
+Reachability analysis of pushdown automata: Application to model-checking
+Normal rank
@@ Property / cites work @@
+SAT-Based Model Checking without Unrolling
@@ Property / cites work: SAT-Based Model Checking without Unrolling / rank @@
+Normal rank
@@ Property / cites work @@
+Understanding IC3
@@ Property / cites work: Understanding IC3 / rank @@
+Normal rank
@@ Property / cites work @@
+An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
+Normal rank
@@ Property / cites work @@
+Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
+Normal rank
@@ Property / cites work @@
+Graph-Based Algorithms for Boolean Function Manipulation
+Normal rank
@@ Property / cites work @@
+Deciding Bit-Vector Arithmetic with Abstraction
@@ Property / cites work: Deciding Bit-Vector Arithmetic with Abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Regular canonical systems
@@ Property / cites work: Regular canonical systems / rank @@
+Normal rank
@@ Property / cites work @@
+Verification of SpecC using predicate abstraction
@@ Property / cites work: Verification of SpecC using predicate abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Predicate abstraction of ANSI-C programs using SAT
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Counterexample-guided abstraction refinement for symbolic model checking
+Normal rank
@@ Property / cites work @@
+Q5227061
@@ Property / cites work: Q5227061 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Natural Domain SMT: A Preliminary Assessment
@@ Property / cites work: Natural Domain SMT: A Preliminary Assessment / rank @@
+Normal rank
@@ Property / cites work @@
+Simplify: a theorem prover for program checking
@@ Property / cites work: Simplify: a theorem prover for program checking / rank @@
+Normal rank
@@ Property / cites work @@
+Strengthening Induction-Based Race Checking with Lightweight Static Analysis
+Normal rank
@@ Property / cites work @@
+Abstract conflict driven learning
@@ Property / cites work: Abstract conflict driven learning / rank @@
+Normal rank
@@ Property / cites work @@
+Numeric Bounds Analysis with Conflict-Driven Learning
+Normal rank
@@ Property / cites work @@
+Exploiting step semantics for efficient bounded model checking of asynchronous systems
+Normal rank
@@ Property / cites work @@
+Applying Logic Synthesis for Speeding Up SAT
@@ Property / cites work: Applying Logic Synthesis for Speeding Up SAT / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Functional Specification of Hardware via Temporal Logic
+Normal rank
@@ Property / cites work @@
+Delay-bounded scheduling
@@ Property / cites work: Delay-bounded scheduling / rank @@
+Normal rank
@@ Property / cites work @@
+Q4223067
@@ Property / cites work: Q4223067 / rank @@
+Normal rank
@@ Property / cites work @@
+SAT-Based Scalable Formal Verification Solutions
@@ Property / cites work: SAT-Based Scalable Formal Verification Solutions / rank @@
+Normal rank
@@ Property / cites work @@
+Q2849596
@@ Property / cites work: Q2849596 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Model Checking Concurrent Programs
@@ Property / cites work: Model Checking Concurrent Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Bounded Model Checking for Weak Alternating Büchi Automata
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Abstractions from proofs
@@ Property / cites work: Abstractions from proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Generalized Property Directed Reachability
@@ Property / cites work: Generalized Property Directed Reachability / rank @@
+Normal rank
@@ Property / cites work @@
+Simulating circuit-level simplifications on CNF
@@ Property / cites work: Simulating circuit-level simplifications on CNF / rank @@
+Normal rank
@@ Property / cites work @@
+Predicate Abstraction for Program Verification
@@ Property / cites work: Predicate Abstraction for Program Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q2845508
@@ Property / cites work: Q2845508 / rank @@
+Normal rank
@@ Property / cites work @@
+Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
+Normal rank
@@ Property / cites work @@
+Symbolic execution and program testing
@@ Property / cites work: Symbolic execution and program testing / rank @@
+Normal rank
@@ Property / cites work @@
+Q2848683
@@ Property / cites work: Q2848683 / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolating Quantifier-Free Presburger Arithmetic
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Linear Completeness Thresholds for Bounded Model Checking
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Loop Summarization Using Abstract Transformers
@@ Property / cites work: Loop Summarization Using Abstract Transformers / rank @@
+Normal rank
@@ Property / cites work @@
+Q4414397
@@ Property / cites work: Q4414397 / rank @@
+Normal rank
@@ Property / cites work @@
+Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
+Normal rank
@@ Property / cites work @@
+Q4326390
@@ Property / cites work: Q4326390 / rank @@
+Normal rank
@@ Property / cites work @@
+Reducing concurrent analysis under a context bound to sequential analysis
+Normal rank
@@ Property / cites work @@
+Formal Methods in Computer-Aided Design
@@ Property / cites work: Formal Methods in Computer-Aided Design / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Q4804900
@@ Property / cites work: Q4804900 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Interpolation and Model Checking
@@ Property / cites work: Interpolation and Model Checking / rank @@
+Normal rank
@@ Property / cites work @@
+Q4417909
@@ Property / cites work: Q4417909 / rank @@
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q3146278
@@ Property / cites work: Q3146278 / rank @@
+Normal rank
@@ Property / cites work @@
+Temporal Logic and Fair Discrete Systems
@@ Property / cites work: Temporal Logic and Fair Discrete Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Planning as satisfiability: heuristics
@@ Property / cites work: Planning as satisfiability: heuristics / rank @@
+Normal rank
@@ Property / cites work @@
+Q3506045
@@ Property / cites work: Q3506045 / rank @@
+Normal rank
@@ Property / cites work @@
+On interference abstractions
@@ Property / cites work: On interference abstractions / rank @@
+Normal rank
@@ Property / cites work @@
+Q5593816
@@ Property / cites work: Q5593816 / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning about infinite computations
@@ Property / cites work: Reasoning about infinite computations / rank @@
+Normal rank