The following pages link to Clark Barrett (Q518400):
Displaying 50 items.
- An efficient SMT solver for string constraints (Q518402) (← links)
- Translation and run-time validation of loop transformations (Q812060) (← links)
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) (Q861691) (← links)
- Solving quantified verification conditions using satisfiability modulo theories (Q1037401) (← links)
- Designing theory solvers with extensions (Q1687536) (← links)
- Deciding local theory extensions via E-matching (Q1702888) (← links)
- Counterexample-guided quantifier instantiation for synthesis in SMT (Q1702893) (← links)
- Datatypes with shared selectors (Q1799121) (← links)
- Counterexample-guided prophecy for model checking modulo the theory of arrays (Q2044196) (← links)
- On solving quantified bit-vector constraints using invertibility conditions (Q2050109) (← links)
- Towards satisfiability modulo parametric bit-vectors (Q2051567) (← links)
- Politeness and stable infiniteness: stronger together (Q2055852) (← links)
- Polite combination of algebraic datatypes (Q2090130) (← links)
- A decision procedure for string to code point conversion (Q2096448) (← links)
- Politeness for the theory of algebraic datatypes (Q2096449) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) (Q2104500) (← links)
- Reasoning about vectors using an SMT theory of sequences (Q2104504) (← links)
- Smt-Switch: a solver-agnostic C++ API for SMT solving (Q2118327) (← links)
- Reluplex: an efficient SMT solver for verifying deep neural networks (Q2151238) (← links)
- SMTCoq: a plug-in for integrating SMT solvers into Coq (Q2164216) (← links)
- Scaling up DPLL(T) string solvers using context-dependent simplification (Q2164248) (← links)
- Syntax-guided rewrite rule enumeration for SMT solvers (Q2181939) (← links)
- DRAT-based bit-vector proofs in CVC4 (Q2181940) (← links)
- Syntax-guided quantifier instantiation (Q2233503) (← links)
- An SMT-based approach for verifying binarized neural networks (Q2233508) (← links)
- Refutation-based synthesis in SMT (Q2280222) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- Towards bit-width-independent proofs in SMT solvers (Q2305428) (← links)
- Book review of: Daniel Kroening and Ofer Strichman, Decision procedures: an algorithmic point of view (Q2351398) (← links)
- Relational constraint solving in SMT (Q2405247) (← links)
- Being careful about theory combination (Q2441773) (← links)
- Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) (Q2461559) (← links)
- (Q2723410) (← links)
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (Q2817912) (← links)
- (Q2844808) (← links)
- (Q2848051) (← links)
- (Q2848053) (← links)
- (Q2848688) (← links)
- An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (Q2864522) (← links)
- A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings (Q2964458) (← links)
- Sharing Is Caring: Combination of Theories (Q3172894) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors (Q3460065) (← links)
- Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors (Q3522062) (← links)
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories (Q3608772) (← links)
- (Q4553283) (← links)
- Constraint solving for finite model finding in SMT solvers (Q4593094) (← links)
- (Q4737130) (← links)
- (Q4804899) (← links)