Boolector
From MaRDI portal
Software:12856
No author found.
Related Items (36)
Partial Order Reduction for Deep Bug Finding in Synchronous Hardware ⋮ Sharing Is Caring: Combination of Theories ⋮ Hardware Trojan detection via rewriting logic ⋮ Satisfiability Modulo Theories ⋮ LCTD: test-guided proofs for C programs on LLVM ⋮ Simulating circuit-level simplifications on CNF ⋮ Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions ⋮ Syntax-guided rewrite rule enumeration for SMT solvers ⋮ Incremental bounded model checking for embedded software ⋮ Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems ⋮ Matching Multiplications in Bit-Vector Formulas ⋮ A bit-vector differential model for the modular addition by a constant ⋮ Exploiting step semantics for efficient bounded model checking of asynchronous systems ⋮ Efficiently solving quantified bit-vector formulas ⋮ Being careful about theory combination ⋮ SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME ⋮ Counterexample-Guided Model Synthesis ⋮ Complexity of fixed-size bit-vector logics ⋮ Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution ⋮ Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Decision procedures. An algorithmic point of view ⋮ Symbolic trajectory evaluation for word-level verification: theory and implementation ⋮ Sharpening constraint programming approaches for bit-vector theory ⋮ URBiVA: Uniform Reduction to Bit-Vector Arithmetic ⋮ EUFORIA: complete software model checking with uninterpreted functions ⋮ A new probabilistic algorithm for approximate model counting ⋮ Optimization modulo the theories of signed bit-vectors and floating-point numbers ⋮ Deciding Bit-Vector Formulas with mcSAT ⋮ Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers ⋮ Optimization modulo the theory of floating-point numbers ⋮ An SMT theory of fixed-point arithmetic ⋮ Solving bitvectors with MCSAT: explanations from bits and pieces ⋮ Nullstellensatz-proofs for multiplier verification ⋮ Array theory of bounded elements and its applications ⋮ Smt-Switch: a solver-agnostic C++ API for SMT solving
This page was built for software: Boolector
