Guiding Craig interpolation with domain-specific abstractions (Q300418): Difference between revisions

@@ Property / describes a project that uses @@
+CSIsat
@@ Property / describes a project that uses: CSIsat / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PeRIPLO
@@ Property / describes a project that uses: PeRIPLO / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+FLATA
@@ Property / describes a project that uses: FLATA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Houdini
@@ Property / describes a project that uses: Houdini / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CPAchecker
@@ Property / describes a project that uses: CPAchecker / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W595779784
@@ Property / OpenAlex ID: W595779784 / rank @@
+Normal rank
@@ Property / cites work @@
+Lazy Abstraction with Interpolants for Arrays
@@ Property / cites work: Lazy Abstraction with Interpolants for Arrays / 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 @@
+A structure to decide reachability in Petri nets
@@ Property / cites work: A structure to decide reachability in Petri nets / rank @@
+Normal rank
@@ Property / cites work @@
+Programs with Lists Are Counter Automata
@@ Property / cites work: Programs with Lists Are Counter Automata / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Verification of Integer Array Programs
@@ Property / cites work: Automatic Verification of Integer Array Programs / 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 @@
+Accelerating Interpolation-Based Model-Checking
@@ Property / cites work: Accelerating Interpolation-Based Model-Checking / rank @@
+Normal rank
@@ Property / cites work @@
+Consistency analysis of decision-making programs
@@ Property / cites work: Consistency analysis of decision-making programs / rank @@
+Normal rank
@@ Property / cites work @@
+Infinite-state invariant checking with IC3 and predicate abstraction
+Normal rank
@@ Property / cites work @@
+Linear reasoning. A new form of the Herbrand-Gentzen theorem
+Normal rank
@@ Property / cites work @@
+Q4530231
@@ Property / cites work: Q4530231 / rank @@
+Normal rank
@@ Property / cites work @@
+Synthesis of Circular Compositional Program Proofs via Abduction
+Normal rank
@@ Property / cites work @@
+Interpolant Strength
@@ Property / cites work: Interpolant Strength / rank @@
+Normal rank
@@ Property / cites work @@
+Q4289279
@@ Property / cites work: Q4289279 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2763999
@@ Property / cites work: Q2763999 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4198056
@@ Property / cites work: Q4198056 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3618853
@@ Property / cites work: Q3618853 / 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 @@
+Playing in the grey area of proofs
@@ Property / cites work: Playing in the grey area of proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Accelerating Interpolants
@@ Property / cites work: Accelerating Interpolants / rank @@
+Normal rank
@@ Property / cites work @@
+Q4997235
@@ Property / cites work: Q4997235 / rank @@
+Normal rank
@@ Property / cites work @@
+On the reachability problem for 5-dimensional vector addition systems
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Vector addition system reachability problem
@@ Property / cites work: Vector addition system reachability problem / rank @@
+Normal rank
@@ Property / cites work @@
+Lazy Abstraction with Interpolants
@@ Property / cites work: Lazy Abstraction with Interpolants / rank @@
+Normal rank
@@ Property / cites work @@
+Quantified Invariant Generation Using an Interpolating Saturation Prover
+Normal rank
@@ Property / cites work @@
+Dual analysis for proving safety and finding bugs
@@ Property / cites work: Dual analysis for proving safety and finding bugs / rank @@
+Normal rank
@@ Property / cites work @@
+An Efficient and Flexible Approach to Resolution Proof Reduction
+Normal rank
@@ Property / cites work @@
+PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification
+Normal rank
@@ Property / cites work @@
+On recursion-free Horn clauses and Craig interpolation
+Normal rank
@@ Property / cites work @@
+Constraint Solving for Interpolation
@@ Property / cites work: Constraint Solving for Interpolation / rank @@
+Normal rank
@@ Property / cites work @@
+A Lightweight Approach for Loop Summarization
@@ Property / cites work: A Lightweight Approach for Loop Summarization / rank @@
+Normal rank
@@ Property / cites work @@
+Complete instantiation-based interpolation
@@ Property / cites work: Complete instantiation-based interpolation / rank @@
+Normal rank