Boolector

swMATH85MaRDI QIDQ12856FDOQ12856

Author name not available (Why is that?)

Cited In (36)

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

This page was built for software: Boolector