CVC4

swMATH9485MaRDI QIDQ21467FDOQ21467

Author name not available (Why is that?)

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)

• Fast Cube Tests for LIA Constraint Solving
• 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
• Checking deadlock-freedom of parametric component-based systems
• TIP: Tools for Inductive Provers
• $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• Equivalence between model-checking flat counter systems and Presburger arithmetic
• Extensional higher-order paramodulation in Leo-III
• The CADE-27 Automated theorem proving System Competition – CASC-27
• Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment
• On solving quantified bit-vector constraints using invertibility conditions
• Towards satisfiability modulo parametric bit-vectors
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Parallelizing SMT solving: lazy decomposition and conciliation
• Making higher-order superposition work
• Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
• Programming and symbolic computation in Maude
• Inductive benchmarks for automated reasoning
• Solving linear optimization over arithmetic constraint formula
• SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME
• 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
• Datatypes with shared selectors
• Superposition with datatypes and codatatypes
• Search-Space Partitioning for Parallelizing SMT Solvers
• 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
• Handling transitive relations in first-order automated reasoning
• New techniques for linear arithmetic: cubes and equalities
• Propagation based local search for bit-precise reasoning
• Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
• Reasoning about algebraic data types with abstractions
• The SDEval benchmarking toolkit
• 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
• Coming to terms with quantified reasoning
• Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
• 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
• Automatic generation of precise and useful commutativity conditions
• A process calculus for privacy-preserving protocols in location-based service systems
• Model Finding for Recursive Functions in SMT
• Building bridges between symbolic computation and satisfiability checking
• Title not available (Why is that?)
• Chain-Free String Constraints
• Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
• Contract-based verification of MATLAB-style matrix programs
• A set solver for finite set relation algebra
• Counterexample-guided quantifier instantiation for synthesis in SMT
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• Beagle – A Hierarchic Superposition Theorem Prover
• MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
• SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
• Decision procedures for flat array properties
• Adding decision procedures to SMT solvers using axioms with triggers
• Semi-intelligible Isar proofs from machine-generated proofs
• The satisfiability of word equations: decidable and undecidable theories
• 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
• Integrating Simplex with Tableaux
• A deontic logic reasoning infrastructure
• String theories involving regular membership predicates: from practice to theory and back
• Cutting the mix
• One Logic to Use Them All
• 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
• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• 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

This page was built for software: CVC4