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