Boolector
From MaRDI portal
Cited in
(88)- 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
- Being careful about theory combination
- URBiVA: uniform reduction to bit-vector arithmetic
- Synthesis of domain specific CNF encoders for bit-vector solvers
- Array theory of bounded elements and its applications
- Parallelizing SMT solving: lazy decomposition and conciliation
- Matching multiplications in bit-vector formulas
- 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
- Beaver
- CPBPV
- POEM
- SMT-LIB
- SATIRE
- Yices
- KLEE
- bv2epr
- OpenSMT
- MathSAT
- MathSAT5
- r-TuBound
- Azucar
- URBiVA
- UML2Alloy
- RSat
- Vellvm
- Smacc
- LCTD
- ICS
- PySMT
- OTAWA
- Kind 2
- STEWord
- BoogiePL
- OSMOSE
- TCAS
- UppSAT
- SymDIVINE
- BINSEC/SE
- AIGER
- petBoss
- TRANSIT
- LCT
- EUFORIA
- OptiMathSAT
- Yosys
- STP
- PolyCleaner
- RevSCA
- QF_FP
- Efficiently solving quantified bit-vector formulas
- Deciding Bit-Vector Formulas with mcSAT
- 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
- Nusschecker
- 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
- AMulet
- Bosphorus
- CoSA
- BtorMC
- Pono
- QBFFam
- Q3B
- Complexity of fixed-size bit-vector logics
- Nullstellensatz-proofs for multiplier verification
- Encoding OCL data types for SAT-based verification of UML/OCL models
- Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution
- Sharpening constraint programming approaches for bit-vector theory
- Counterexample-Guided Model Synthesis
- Decision procedures. An algorithmic point of view
- Smt-Switch: a solver-agnostic C++ API for SMT solving
- Pacheck
- Jasmin
- OPTGEN
- Symbolic trajectory evaluation for word-level verification: theory and implementation
This page was built for software: Boolector
