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
• Synthesizing precise and useful commutativity conditions
• Witness Runs for Counter Machines
• \textsc{Hampa}: solver-aided recency-aware replication
• Set Constraints, Pattern Match Analysis, and SMT
• Title not available (Why is that?)
• Deductive verification of floating-point Java programs in KeY
• Reducing bit-vector polynomials to SAT using Gröbner bases
• Verifying and Synthesizing Software with Recursive Functions
• On Symbolic Heaps Modulo Permission Theories
• A Generic Intermediate Representation for Verification Condition Generation
• Symbolic automatic relations and their applications to SMT and CHC solving
• Program Verification with Separation Logic
• Generalized arrays for Stainless frames
• Satisfiability and synthesis modulo oracles
• GRUNGE: a grand unified ATP challenge
• Word equations in the context of string solving
• Translating Scala Programs to Isabelle/HOL
• Witness Runs for Counter Machines
• Making higher-order superposition work
• Effective Normalization Techniques for HOL
• Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Separation logic with one quantified variable
• SMT-based generation of symbolic automata
• Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
• Higher order symbolic execution for contract verification and refutation
• Automating free logic in HOL, with an experimental application in category theory
• Two Decades of Maude
• A complete and terminating approach to linear integer solving
• Modular strategic SMT solving with \textbf{SMT-RAT}
• 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

This page was built for software: CVC4