swMATH85MaRDI QIDQ12856FDOQ12856
Author name not available (Why is that?)
Official website: http://fmv.jku.at/boolector/
Cited In (85)
- Nusschecker
- Partial order reduction for deep bug finding in synchronous hardware
- URBiVA: uniform reduction to bit-vector arithmetic
- Being careful about theory combination
- 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
- Synthesis of domain specific CNF encoders for bit-vector solvers
- Jasmin
- 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
- OPTGEN
- A bit-vector differential model for the modular addition by a constant
- Deciding Bit-Vector Formulas with mcSAT
- Efficiently solving quantified bit-vector formulas
- SMT-LIB
- SATIRE
- Yices
- KLEE
- bv2epr
- OpenSMT
- MathSAT
- MathSAT5
- r-TuBound
- Azucar
- URBiVA
- UML2Alloy
- RSat
- Vellvm
- Smacc
- LCTD
- LCTD: test-guided proofs for C programs on LLVM
- ICS
- PySMT
- OTAWA
- Kind 2
- STEWord
- BoogiePL
- OSMOSE
- TCAS
- UppSAT
- SymDIVINE
- BINSEC/SE
- AIGER
- petBoss
- TRANSIT
- LCT
- EUFORIA
- OptiMathSAT
- Yosys
- STP
- 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
- PolyCleaner
- RevSCA
- QF_FP
- 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
- AMulet
- Bosphorus
- CoSA
- BtorMC
- Pono
- QBFFam
- Q3B
- Nullstellensatz-proofs for multiplier verification
- Complexity of fixed-size bit-vector logics
- Encoding OCL data types for SAT-based verification of UML/OCL models
- Pacheck
- 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
