The following pages link to CVC4 (Q21467):
Displaying 50 items.
- Integer induction in saturation (Q2055871) (← links)
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (Q2058375) (← links)
- Handling transitive relations in first-order automated reasoning (Q2069868) (← links)
- Induction and Skolemization in saturation theorem proving (Q2084957) (← links)
- Polite combination of algebraic datatypes (Q2090130) (← links)
- An SMT theory of fixed-point arithmetic (Q2096435) (← links)
- Removing algebraic data types from constrained Horn clauses using difference predicates (Q2096439) (← links)
- Scalable algorithms for abduction via enumerative syntax-guided synthesis (Q2096443) (← links)
- A decision procedure for string to code point conversion (Q2096448) (← links)
- Subsumption demodulation in first-order theorem proving (Q2096454) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- CTL* model checking for data-aware dynamic systems with arithmetic (Q2104496) (← links)
- Reasoning about vectors using an SMT theory of sequences (Q2104504) (← links)
- Smt-Switch: a solver-agnostic C++ API for SMT solving (Q2118327) (← links)
- MedleySolver: online SMT algorithm selection (Q2118336) (← links)
- Inductive benchmarks for automated reasoning (Q2128807) (← links)
- String theories involving regular membership predicates: from practice to theory and back (Q2140459) (← links)
- Symbolic automatic relations and their applications to SMT and CHC solving (Q2145347) (← links)
- Correct approximation of IEEE 754 floating-point arithmetic for program verification (Q2152274) (← links)
- Satisfiability and synthesis modulo oracles (Q2152655) (← links)
- Generalized arrays for Stainless frames (Q2152661) (← links)
- Word equations in the context of string solving (Q2163975) (← links)
- A neurally-guided, parallel theorem prover (Q2180215) (← links)
- Syntax-guided rewrite rule enumeration for SMT solvers (Q2181939) (← links)
- DRAT-based bit-vector proofs in CVC4 (Q2181940) (← links)
- SMT-based generation of symbolic automata (Q2182674) (← links)
- Synthesizing precise and useful commutativity conditions (Q2208295) (← links)
- \textsc{Hampa}: solver-aided recency-aware replication (Q2225111) (← links)
- Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
- Refutation-based synthesis in SMT (Q2280222) (← links)
- Programming and symbolic computation in Maude (Q2291818) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- SPASS-SATT. A CDCL(LA) solver (Q2305409) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- Towards bit-width-independent proofs in SMT solvers (Q2305428) (← links)
- A complete and terminating approach to linear integer solving (Q2307624) (← links)
- Unification with abstraction and theory instantiation in saturation-based reasoning (Q2324203) (← links)
- Automatic generation of precise and useful commutativity conditions (Q2324210) (← links)
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (Q2360872) (← links)
- A decision procedure for (co)datatypes in SMT solvers (Q2360873) (← links)
- Monte Carlo tableau proof search (Q2405274) (← links)
- Separation logic with one quantified variable (Q2411038) (← links)
- Modular strategic SMT solving with \textbf{SMT-RAT} (Q2414693) (← links)
- Equivalence between model-checking flat counter systems and Presburger arithmetic (Q2636509) (← links)
- Reducing bit-vector polynomials to SAT using Gröbner bases (Q2661363) (← links)
- Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions (Q2661364) (← links)
