Boolector
From MaRDI portal
Cited in
(88)- Hardware Trojan detection via rewriting logic
- Array theory of bounded elements and its applications
- Deciding Bit-Vector Formulas with mcSAT
- Efficiently solving quantified 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
- Jasmin
- Optimization modulo the theories of signed bit-vectors and floating-point numbers
- Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems
- Syntax-guided rewrite rule enumeration for SMT solvers
- Simulating circuit-level simplifications on CNF
- A new probabilistic algorithm for approximate model counting
- Counterexample-Guided Model Synthesis
- Optimization modulo the theory of floating-point numbers
- Beaver
- CPBPV
- POEM
- SMT-LIB
- SATIRE
- Yices
- KLEE
- bv2epr
- OpenSMT
- MathSAT
- MathSAT5
- r-TuBound
- Azucar
- URBiVA
- UML2Alloy
- RSat
- Vellvm
- Smacc
- LCTD
- Incremental bounded model checking for embedded software
- Matching multiplications in bit-vector formulas
- Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions
- 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
- Parallelizing SMT solving: lazy decomposition and conciliation
- Nullstellensatz-proofs for multiplier verification
- An SMT theory of fixed-point arithmetic
- Solving bitvectors with MCSAT: explanations from bits and pieces
- SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME
- Decision procedures. An algorithmic point of view
- Synthesis of domain specific CNF encoders for bit-vector solvers
- AMulet
- Bosphorus
- CoSA
- BtorMC
- Pono
- QBFFam
- Q3B
- Sharpening constraint programming approaches for bit-vector theory
- Symbolic trajectory evaluation for word-level verification: theory and implementation
- Complexity of fixed-size bit-vector logics
- Pacheck
- Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution
- LCTD: test-guided proofs for C programs on LLVM
- EUFORIA: complete software model checking with uninterpreted functions
- Encoding OCL data types for SAT-based verification of UML/OCL models
- Satisfiability modulo theories
- Smt-Switch: a solver-agnostic C++ API for SMT solving
- Nusschecker
- Partial order reduction for deep bug finding in synchronous hardware
- OPTGEN
- URBiVA: uniform reduction to bit-vector arithmetic
- Sharing is caring: combination of theories
- Being careful about theory combination
This page was built for software: Boolector
