Cited in
(only showing first 100 items - show all)- Loop Invariants from Counterexamples
- Integrating simplex with tableaux
- Synthesizing precise and useful commutativity conditions
- On equations and first-order theory of one-relator monoids
- SeLoger
- 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 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 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
- Coming to terms with quantified reasoning
- Automatic generation of precise and useful commutativity conditions
- A process calculus for privacy-preserving protocols in location-based service systems
- A neurally-guided, parallel theorem prover
- LocLok
- MaPIR
- \textsc{Hampa}: solver-aided recency-aware replication
- Checking deadlock-freedom of parametric component-based systems
- Building bridges between symbolic computation and satisfiability checking
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Contract-based verification of MATLAB-style matrix programs
- Synthesis of domain specific CNF encoders for bit-vector solvers
- Equivalence between model-checking flat counter systems and Presburger arithmetic
- A set solver for finite set relation algebra
- Extensional higher-order paramodulation in Leo-III
- The \textsc{SDEval} benchmarking toolkit
- scientific article; zbMATH DE number 7453193 (Why is no real title available?)
- Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment
- Deductive verification of floating-point Java programs in KeY
- On solving quantified bit-vector constraints using invertibility conditions
- Towards satisfiability modulo parametric bit-vectors
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Decision procedures for flat array properties
- Adding decision procedures to SMT solvers using axioms with triggers
- Semi-intelligible Isar proofs from machine-generated proofs
- Reducing bit-vector polynomials to SAT using Gröbner bases
- The satisfiability of word equations: decidable and undecidable theories
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Parallelizing SMT solving: lazy decomposition and conciliation
- Matching multiplications in bit-vector formulas
- Polyhedral approximation of multivariate polynomials using Handelman's theorem
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- TIP: tons of inductive problems
- Extensional crisis and proving identity
- Solving nonlinear integer arithmetic with MCSAT
- Congruence closure with free variables
- Search-space partitioning for parallelizing SMT solvers
- Incomplete SMT techniques for solving non-linear formulas over the integers
- Translating Scala programs to Isabelle/HOL. System description
- 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
- Witness runs for counter machines
- An SMT theory of fixed-point arithmetic
- A deontic logic reasoning infrastructure
- String theories involving regular membership predicates: from practice to theory and back
- Cutting the mix
- Making higher-order superposition work
- DRAT-based bit-vector proofs in CVC4
- Refutation-based synthesis in SMT
- SPASS-SATT. A CDCL(LA) solver
- Effective normalization techniques for HOL
- On Symbolic Heaps Modulo Permission Theories
- Instrumenting a weakest precondition calculus for counterexample generation
- Monte Carlo tableau proof search
- Symbolic automatic relations and their applications to SMT and CHC solving
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- Apron
- Beaver
- Boolector
- CoCoALib
- CPBPV
- CUTE
- Dafny
- D-Finder
- LEO-II
- MiniSat
- Nitpick
- SDSAT
- SYNRAC
- LOGEN
- VAMPIRE
- Paradox
- SMT-LIB
- REDLOG
- SPASS
- TPTP
- Punf
- Frama-C
- SATIRE
This page was built for software: CVC4
