CVC4
From MaRDI portal
Software:21467
swMATH9485MaRDI QIDQ21467FDOQ21467
Author name not available (Why is that?)
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