The following pages link to CVC4 (Q21467):
Displaying 45 items.
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- Decision procedures for flat array properties (Q287272) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Adding decision procedures to SMT solvers using axioms with triggers (Q287384) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- An efficient SMT solver for string constraints (Q518402) (← links)
- Decision procedures. An algorithmic point of view (Q518892) (← links)
- Symbolic trajectory evaluation for word-level verification: theory and implementation (Q526779) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- Symbol elimination and applications to parametric entailment problems (Q831921) (← links)
- Quantifier simplification by unification in SMT (Q831945) (← links)
- Not all bugs are created equal, but robust reachability can tell the difference (Q832220) (← links)
- Counterexample-guided partial bounding for recursive function synthesis (Q832233) (← links)
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver (Q832260) (← links)
- An SMT solver for regular expressions and linear arithmetic over string length (Q832270) (← links)
- A set solver for finite set relation algebra (Q1617837) (← links)
- A formally verified interpreter for a shell-like programming language (Q1630019) (← links)
- Instrumenting a weakest precondition calculus for counterexample generation (Q1648649) (← links)
- Computing and estimating the volume of the solution space of SMT(LA) constraints (Q1659994) (← links)
- A deontic logic reasoning infrastructure (Q1670720) (← links)
- Solving linear optimization over arithmetic constraint formula (Q1675635) (← links)
- Automatically improving constraint models in Savile Row (Q1680696) (← links)
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (Q1687709) (← links)
- New techniques for linear arithmetic: cubes and equalities (Q1688532) (← links)
- Propagation based local search for bit-precise reasoning (Q1688546) (← links)
- Reasoning about algebraic data types with abstractions (Q1694026) (← links)
- Cutting the mix (Q1702886) (← links)
- Counterexample-guided quantifier instantiation for synthesis in SMT (Q1702893) (← links)
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (Q1735326) (← links)
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (Q1739908) (← links)
- Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment (Q1742627) (← links)
- Parallelizing SMT solving: lazy decomposition and conciliation (Q1749390) (← links)
- Positive solutions of systems of signed parametric polynomial inequalities (Q1798326) (← links)
- Unifying separation logic and region logic to allow interoperability (Q1798668) (← links)
- The satisfiability of word equations: decidable and undecidable theories (Q1798903) (← links)
- A generic framework for implicate generation modulo theories (Q1799090) (← links)
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems (Q1799091) (← links)
- A reduction from unbounded linear mixed arithmetic problems into bounded problems (Q1799094) (← links)
- Superposition with datatypes and codatatypes (Q1799098) (← links)
- Datatypes with shared selectors (Q1799121) (← links)
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays (Q5043584) (← links)
- On Symbolic Heaps Modulo Permission Theories (Q5136317) (← links)
- Loop Analysis by Quantification over Iterations (Q5222968) (← links)
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker (Q5883751) (← links)