The following pages link to Cesare Tinelli (Q429585):
Displaying 50 items.
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- An efficient SMT solver for string constraints (Q518402) (← links)
- Combining nonstably infinite theories (Q851136) (← links)
- Computing finite models by reduction to function-free clause logic (Q1006733) (← links)
- Solving quantified verification conditions using satisfiability modulo theories (Q1037401) (← links)
- Deciding the word problem in the union of equational theories. (Q1400706) (← links)
- Designing theory solvers with extensions (Q1687536) (← links)
- Counterexample-guided quantifier instantiation for synthesis in SMT (Q1702893) (← links)
- Datatypes with shared selectors (Q1799121) (← links)
- Cooperation of background reasoners in theory reasoning by residue sharing (Q1810855) (← links)
- Unions of non-disjoint theories and combinations of satisfiability procedures (Q1853591) (← 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)
- Scalable algorithms for abduction via enumerative syntax-guided synthesis (Q2096443) (← links)
- A decision procedure for string to code point conversion (Q2096448) (← 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)
- 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)
- A tour of Franz Baader's contributions to knowledge representation and automated deduction (Q2185456) (← links)
- Theory combination: beyond equality sharing (Q2185458) (← links)
- Syntax-guided quantifier instantiation (Q2233503) (← 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)
- The model evolution calculus as a first-order DPLL method (Q2389629) (← links)
- Relational constraint solving in SMT (Q2405247) (← links)
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics (Q2432763) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (Q2817912) (← links)
- Model Finding for Recursive Functions in SMT (Q2817915) (← links)
- An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types (Q2864522) (← links)
- Ground interpolation for the theory of equality (Q2881073) (← links)
- A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings (Q2964458) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- Solving SAT and SAT Modulo Theories (Q3455223) (← links)
- Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors (Q3460065) (← links)
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories (Q3608772) (← links)
- Ground Interpolation for the Theory of Equality (Q3617772) (← links)
- (Q4259971) (← links)
- (Q4385439) (← links)
- (Q4518874) (← links)
- (Q4553283) (← links)
- Constraint solving for finite model finding in SMT solvers (Q4593094) (← links)
- (Q4708927) (← links)
- (Q4808758) (← links)
