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
• Coming to terms with quantified reasoning
• Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• Counterexample-guided partial bounding for recursive function synthesis
• An SMT solver for regular expressions and linear arithmetic over string length
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• Not all bugs are created equal, but robust reachability can tell the difference
• Quantifier simplification by unification in SMT
• Symbol elimination and applications to parametric entailment problems
• A process calculus for privacy-preserving protocols in location-based service systems
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• A set solver for finite set relation algebra
• Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment
• The satisfiability of word equations: decidable and undecidable theories
• Parallelizing SMT solving: lazy decomposition and conciliation
• TIP: tons of inductive problems
• Extensional crisis and proving identity
• Polyhedral approximation of multivariate polynomials using Handelman's theorem
• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• Solving nonlinear integer arithmetic with MCSAT
• Incomplete SMT techniques for solving non-linear formulas over the integers
• Search-space partitioning for parallelizing SMT solvers
• Congruence closure with free variables
• Simpler proofs with decentralized invariants
• Algorithmic reduction of biological networks with multiple time scales
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• An SMT theory of fixed-point arithmetic
• A deontic logic reasoning infrastructure
• String theories involving regular membership predicates: from practice to theory and back
• DRAT-based bit-vector proofs in CVC4
• Refutation-based synthesis in SMT
• SPASS-SATT. A CDCL(LA) solver
• Monte Carlo tableau proof search
• Instrumenting a weakest precondition calculus for counterexample generation
• Towards more efficient methods for solving regular-expression heavy string constraints
• Subsumption demodulation in first-order theorem proving
• Computing and estimating the volume of the solution space of SMT(LA) constraints
• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• Deciding Bit-Vector Formulas with mcSAT
• Reasoning with finite sets and cardinality constraints in SMT
• Congruence closure in intensional type theory
• Solving linear optimization over arithmetic constraint formula
• Positive solutions of systems of signed parametric polynomial inequalities
• A generic framework for implicate generation modulo theories
• A reduction from unbounded linear mixed arithmetic problems into bounded problems
• Unifying separation logic and region logic to allow interoperability
• Superposition with datatypes and codatatypes
• Automatically improving constraint models in Savile Row
• New techniques for linear arithmetic: cubes and equalities

This page was built for software: CVC4