On recursion-free Horn clauses and Craig interpolation (Q746767): Difference between revisions

@@ Property / cites work @@
+Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
+Normal rank
@@ Property / cites work @@
+Q4472235
@@ Property / cites work: Q4472235 / rank @@
+Normal rank
@@ Property / cites work @@
+Analysis of Linear Hybrid Systems in CLP
@@ Property / cites work: Analysis of Linear Hybrid Systems in CLP / rank @@
+Normal rank
@@ Property / cites work @@
+Q5015366
@@ Property / cites work: Q5015366 / rank @@
+Normal rank
@@ Property / cites work @@
+An interpolating sequent calculus for quantifier-free Presburger arithmetic
+Normal rank
@@ Property / cites work @@
+Efficient generation of craig interpolants in satisfiability modulo theories
+Normal rank
@@ Property / cites work @@
+Linear reasoning. A new form of the Herbrand-Gentzen theorem
+Normal rank
@@ Property / cites work @@
+Synthesis of Circular Compositional Program Proofs via Abduction
+Normal rank
@@ Property / cites work @@
+Generalization strategies for the verification of infinite state systems
+Normal rank
@@ Property / cites work @@
+Analysis of Boolean Programs
@@ Property / cites work: Analysis of Boolean Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Predicate abstraction and refinement for verifying multi-threaded programs
+Normal rank
@@ Property / cites work @@
+Q4997234
@@ Property / cites work: Q4997234 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic-based program synthesis and transformation. 18th international symposium, LOPSTR 2008, Valencia, Spain, July 17--18, 2008. Revised selected papers
+Normal rank
@@ Property / cites work @@
+Nested interpolants
@@ Property / cites work: Nested interpolants / 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 @@
+Accelerating Interpolants
@@ Property / cites work: Accelerating Interpolants / rank @@
+Normal rank
@@ Property / cites work @@
+Q4997236
@@ Property / cites work: Q4997236 / rank @@
+Normal rank
@@ Property / cites work @@
+SMT-based model checking for recursive programs
@@ Property / cites work: SMT-based model checking for recursive programs / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Lazy Abstraction with Interpolants
@@ Property / cites work: Lazy Abstraction with Interpolants / rank @@
+Normal rank
@@ Property / cites work @@
+A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
+Normal rank
@@ Property / cites work @@
+On recursion-free Horn clauses and Craig interpolation
+Normal rank
@@ Property / cites work @@
+Computer aided verification. 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings
+Normal rank
@@ Property / cites work @@
+Dependent types from counterexamples
@@ Property / cites work: Dependent types from counterexamples / rank @@
+Normal rank
@@ Property / cites work @@
+Automating relatively complete verification of higher-order functional programs
+Normal rank