CVC4

swMATH9485MaRDI QIDQ21467FDOQ21467

Author name not available (Why is that?)

Official website: http://cvc4.cs.nyu.edu/web/

Described by source

• Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
• Induction for SMT solvers

Cited In (only showing first 100 items - show all)

• Synthesizing precise and useful commutativity conditions
• On equations and first-order theory of one-relator monoids
• A posthumous contribution by Larry Wos: excerpts from an unpublished column
• Verifying Whiley programs with Boogie
• CTL* model checking for data-aware dynamic systems with arithmetic
• Flexible proof production in an industrial-strength SMT solver
• Reasoning about vectors using an SMT theory of sequences
• A neurally-guided, parallel theorem prover
• \textsc{Hampa}: solver-aided recency-aware replication
• Checking deadlock-freedom of parametric component-based systems
• Synthesis of domain specific CNF encoders for bit-vector solvers
• The \textsc{SDEval} benchmarking toolkit
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Extensional higher-order paramodulation in Leo-III
• Deductive verification of floating-point Java programs in KeY
• On solving quantified bit-vector constraints using invertibility conditions
• Towards satisfiability modulo parametric bit-vectors
• Zephyrus2
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Making higher-order superposition work
• Symbolic automatic relations and their applications to SMT and CHC solving
• Generalized arrays for Stainless frames
• Satisfiability and synthesis modulo oracles
• GRUNGE: a grand unified ATP challenge
• Word equations in the context of string solving
• Solving quantified bit-vector formulas using binary decision diagrams
• Programming and symbolic computation in Maude
• The CADE-27 automated theorem proving system competition -- CASC-27
• Inductive benchmarks for automated reasoning
• Verifying and synthesizing software with recursive functions (invited contribution)
• SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME
• Datatypes with shared selectors
• Syntax-guided rewrite rule enumeration for SMT solvers
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Towards bit-width-independent proofs in SMT solvers
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Separation logic with one quantified variable
• Handling transitive relations in first-order automated reasoning
• SMT-based generation of symbolic automata
• CertiStr
• Higher order symbolic execution for contract verification and refutation
• Counterexample-Guided Model Synthesis
• Induction and Skolemization in saturation theorem proving
• Computing Parameterized Invariants of Parameterized Petri Nets
• Synthesis of distributed algorithms with parameterized threshold guards
• Polite combination of algebraic datatypes
• A decision procedure for string to code point conversion
• Removing algebraic data types from constrained Horn clauses using difference predicates
• Scalable algorithms for abduction via enumerative syntax-guided synthesis
• Combining induction and saturation-based theorem proving
• eThor
• Casper*
• SpaceTwist
• Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
• Automatic generation of precise and useful commutativity conditions
• Building bridges between symbolic computation and satisfiability checking
• Kissat
• Paracooba
• Contract-based verification of MATLAB-style matrix programs
• Counterexample-guided quantifier instantiation for synthesis in SMT
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• Decision procedures for flat array properties
• Adding decision procedures to SMT solvers using axioms with triggers
• Semi-intelligible Isar proofs from machine-generated proofs
• Matching multiplications in bit-vector formulas
• Cutting the mix
• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• Boolector
• D-Finder
• LEO-II
• SDSAT
• SMT-LIB
• SPASS
• Punf
• Frama-C
• SATIRE
• Why3
• Yices
• CPGraph
• Cunf
• Leon
• Mole
• CBMC
• Cumapz
• Stranger
• Eldarica
• iProver
• InvGen
• Ocelot
• MFE
• WhyML
• FOCI
• CArL
• SMT-RAT
• LeoPARD
• FunArray
• SynchAADL2Maude
• A learning-based fact selector for Isabelle/HOL
• PASS
• HALO

This page was built for software: CVC4