Boolector

swMATH85MaRDI QIDQ12856FDOQ12856

Author name not available (Why is that?)

Cited In (36)

• Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions
• EUFORIA: complete software model checking with uninterpreted functions
• Partial order reduction for deep bug finding in synchronous hardware
• URBiVA: uniform reduction to bit-vector arithmetic
• Being careful about theory combination
• Synthesis of domain specific CNF encoders for bit-vector solvers
• Array theory of bounded elements and its applications
• Matching multiplications in bit-vector formulas
• 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
• A bit-vector differential model for the modular addition by a constant
• Deciding Bit-Vector Formulas with mcSAT
• Efficiently solving quantified bit-vector formulas
• LCTD: test-guided proofs for C programs on LLVM
• Satisfiability modulo theories
• 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
• Syntax-guided rewrite rule enumeration for SMT solvers
• Simulating circuit-level simplifications on CNF
• Incremental bounded model checking for embedded software
• Sharing is caring: combination of theories
• 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
• Encoding OCL data types for SAT-based verification of UML/OCL models
• 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
• 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