The following pages link to Computer Aided Verification (Q5312898):
Displaying 50 items.
- Proof tree preserving tree interpolation (Q286737) (← links)
- Deciding floating-point logic with abstract conflict driven clause learning (Q479837) (← links)
- Parametrized invariance for infinite state processes (Q493122) (← links)
- A search-based procedure for nonlinear real arithmetic (Q518407) (← links)
- Decision procedures. An algorithmic point of view (Q518892) (← links)
- SCIP: solving constraint integer programs (Q734351) (← links)
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) (Q861691) (← links)
- Applying SAT solving in classification of finite algebras (Q862393) (← links)
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures (Q862395) (← links)
- Fast congruence closure and extensions (Q876046) (← links)
- A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures (Q877828) (← links)
- Automatic construction and verification of isotopy invariants (Q928664) (← links)
- CPBPV: a constraint-programming framework for bounded program verification (Q968353) (← links)
- Deciding effectively propositional logic using DPLL and substitution sets (Q972432) (← links)
- A framework for satisfiability modulo theories (Q1037239) (← links)
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (Q1037399) (← links)
- Solving quantified verification conditions using satisfiability modulo theories (Q1037401) (← links)
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates (Q2031420) (← links)
- Dashed strings for string constraint solving (Q2046015) (← links)
- Subsumption demodulation in first-order theorem proving (Q2096454) (← links)
- Automated generation of exam sheets for automated deduction (Q2128822) (← links)
- The SAT+CAS method for combinatorial search with applications to best matrices (Q2294574) (← links)
- SPASS-SATT. A CDCL(LA) solver (Q2305409) (← links)
- Applying computer algebra systems with SAT solvers to the Williamson conjecture (Q2307627) (← links)
- SMELS: satisfiability modulo equality with lazy superposition (Q2351265) (← links)
- A decision procedure for (co)datatypes in SMT solvers (Q2360873) (← links)
- Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint (Q2398511) (← links)
- Efficient theory combination via Boolean search (Q2432765) (← links)
- Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) (Q2461559) (← links)
- Generalizing DPLL and satisfiability for equalities (Q2643080) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- Rewrite-based decision procedures (Q2864358) (← links)
- Generating minimum transitivity constraints in P-time for deciding equality logic (Q2864399) (← links)
- Model-based theory combination (Q2864402) (← links)
- Distributing the workload in a lazy theorem-prover (Q2870323) (← links)
- Decision Procedures for Region Logic (Q2891431) (← links)
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic (Q2961583) (← links)
- Weakly Equivalent Arrays (Q2964457) (← links)
- Solving finite-domain linear constraints in presence of the $\texttt{alldifferent}$ (Q2974776) (← links)
- A Lambda-Free Higher-Order Recursive Path Order (Q2988386) (← links)
- Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models (Q3012970) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- A Decision Procedure for (Co)datatypes in SMT Solvers (Q3454092) (← links)
- Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver (Q3510788) (← links)
- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems (Q3540072) (← links)
- Combining Equational Reasoning (Q3655192) (← links)
- Harald Ganzinger’s Legacy: Contributions to Logics and Programming (Q4916069) (← links)
- EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas (Q4982077) (← links)
- Volume Computation for Boolean Combination of Linear Arithmetic Constraints (Q5191119) (← links)
- Computer Aided Verification (Q5312896) (← links)
