The following pages link to Boolector (Q12856):
Displaying 36 items.
- LCTD: test-guided proofs for C programs on LLVM (Q338629) (← links)
- Simulating circuit-level simplifications on CNF (Q352967) (← links)
- Exploiting step semantics for efficient bounded model checking of asynchronous systems (Q436411) (← links)
- Complexity of fixed-size bit-vector logics (Q504997) (← links)
- Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution (Q507359) (← links)
- Decision procedures. An algorithmic point of view (Q518892) (← links)
- Symbolic trajectory evaluation for word-level verification: theory and implementation (Q526779) (← links)
- Incremental bounded model checking for embedded software (Q1682291) (← links)
- Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems (Q1688718) (← links)
- Parallelizing SMT solving: lazy decomposition and conciliation (Q1749390) (← links)
- A new probabilistic algorithm for approximate model counting (Q1799093) (← links)
- Sharpening constraint programming approaches for bit-vector theory (Q2011567) (← links)
- Optimization modulo the theories of signed bit-vectors and floating-point numbers (Q2051569) (← links)
- An SMT theory of fixed-point arithmetic (Q2096435) (← links)
- Solving bitvectors with MCSAT: explanations from bits and pieces (Q2096440) (← links)
- Nullstellensatz-proofs for multiplier verification (Q2110233) (← links)
- Smt-Switch: a solver-agnostic C++ API for SMT solving (Q2118327) (← links)
- Hardware Trojan detection via rewriting logic (Q2141287) (← links)
- Syntax-guided rewrite rule enumeration for SMT solvers (Q2181939) (← links)
- EUFORIA: complete software model checking with uninterpreted functions (Q2287098) (← links)
- Optimization modulo the theory of floating-point numbers (Q2305439) (← links)
- Array theory of bounded elements and its applications (Q2351149) (← links)
- Efficiently solving quantified bit-vector formulas (Q2441770) (← links)
- Being careful about theory combination (Q2441773) (← links)
- Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions (Q2661364) (← links)
- A bit-vector differential model for the modular addition by a constant (Q2692348) (← links)
- Deciding Bit-Vector Formulas with mcSAT (Q2818018) (← links)
- Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers (Q2818024) (← links)
- Matching Multiplications in Bit-Vector Formulas (Q2961559) (← links)
- Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models (Q3012970) (← links)
- Sharing Is Caring: Combination of Theories (Q3172894) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- Counterexample-Guided Model Synthesis (Q3303898) (← links)
- SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME (Q4621226) (← links)
- Partial Order Reduction for Deep Bug Finding in Synchronous Hardware (Q5039518) (← links)
- URBiVA: Uniform Reduction to Bit-Vector Arithmetic (Q5747772) (← links)
