Parallelizing SMT solving: lazy decomposition and conciliation (Q1749390): Difference between revisions

@@ Property / cites work @@
+Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
+Normal rank
@@ Property / cites work @@
+Q4138187
@@ Property / cites work: Q4138187 / 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 @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+A Decision Procedure for Bit-Vectors and Arrays
@@ Property / cites work: A Decision Procedure for Bit-Vectors and Arrays / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22--29, 2009. Proceedings
+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. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
+Normal rank
@@ Property / cites work @@
+The MathSAT5 SMT Solver
@@ Property / cites work: The MathSAT5 SMT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+Logic in Computer Science
@@ Property / cites work: Logic in Computer Science / rank @@
+Normal rank
@@ Property / cites work @@
+Fast Decision Procedures Based on Congruence Closure
+Normal rank
@@ Property / cites work @@
+Linear reasoning. A new form of the Herbrand-Gentzen theorem
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation and Symbol Elimination
@@ Property / cites work: Interpolation and Symbol Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+An interpolating theorem prover
@@ Property / cites work: An interpolating theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Ground interpolation for the theory of equality
@@ Property / cites work: Ground interpolation for the theory of equality / rank @@
+Normal rank
@@ Property / cites work @@
+An interpolating sequent calculus for quantifier-free Presburger arithmetic
+Normal rank
@@ Property / cites work @@
+Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
+Normal rank
@@ Property / cites work @@
+Efficient generation of craig interpolants in satisfiability modulo theories
+Normal rank
@@ Property / cites work @@
+Constraint solving for interpolation
@@ Property / cites work: Constraint solving for interpolation / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Quantifier-free interpolation in combinations of equality interpolating theories
+Normal rank
@@ Property / cites work @@
+Computer aided verification. 21st international conference, CAV 2009, Grenoble, France, June 26--July 2, 2009. Proceedings
+Normal rank
@@ Property / cites work @@
+Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic
+Normal rank
@@ Property / cites work @@
+Automated reasoning and exhaustive search: Quasigroup existence problems
+Normal rank
@@ Property / cites work @@
+Solvable cases of the decision problem
@@ Property / cites work: Solvable cases of the decision problem / rank @@
+Normal rank
@@ Property / cites work @@
+Exploiting Symmetry in SMT Problems
@@ Property / cites work: Exploiting Symmetry in SMT Problems / rank @@
+Normal rank
@@ Property / cites work @@
+Q3639756
@@ Property / cites work: Q3639756 / rank @@
+Normal rank
@@ Property / cites work @@
+PSATO: A distributed propositional prover and its application to quasigroup problems
+Normal rank
@@ Property / cites work @@
+Counterexample-guided abstraction refinement for symbolic model checking
+Normal rank
@@ Property / cites work @@
+Lazy abstraction
@@ Property / cites work: Lazy abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Lazy Abstraction with Interpolants
@@ Property / cites work: Lazy Abstraction with Interpolants / rank @@
+Normal rank
@@ Property / cites work @@
+Compression of Propositional Resolution Proofs by Lowering Subproofs
+Normal rank
@@ Property / cites work @@
+Two Techniques for Minimizing Resolution Proofs
@@ Property / cites work: Two Techniques for Minimizing Resolution Proofs / rank @@
+Normal rank