Boolector

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