Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays

No abstract is available for this paper.

• Publication year

  2009

• Venue

  International Conference on Tools and Algorithms for Construction and Analysis of Systems

• Publication date

  2009-03-27

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/978-3-642-00768-2_16
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• PicoSAT Essentials

  2008cited by this paper
• Lemmas on Demand for the Extensional Theory of Arrays

  2008cited by this paper
• Z3: An Efficient SMT Solver

  2008cited by this paper
• The Birth of Model Checking

  2008cited by this paper
• 25 Years of Model Checking - History, Achievements, Perspectives

  2008cited by this paper
• Exploiting structure for scalable software verification

  2008cited by this paper
• BTOR: bit-precise modelling of word-level problems for model checking

  2008cited by this paper
• The calculus of computation - decision procedures with applications to verification

  2007cited by this paper
• A Temporal Logic of Nested Calls and Returns

  2004cited by this paper
• Lemmas on Demand for Satisfiability Solvers

  2002cited by this paper
• and as an in

  year unknowncited by this paper

• Synthesis of Code-Reuse Attacks from p-code Programs

  2025cites this paper
• Interactive Bitvector Reasoning using Verified Bit-Blasting

  2025cites this paper
• The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee

  2025cites this paper
• FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping

  2025cites this paper
• Bounded Model Checking of RISC-V Machine Code with Context-Free-Language Ordered Binary Decision Diagrams

  2025cites this paper
• Approximate SMT Counting Beyond Discrete Domains

  2025cites this paper
• Efficient Volume Computation for SMT Formulas

  2025cites this paper
• Formally Verifying the State Machine of TLS 1.3 Handshake in OpenSSL

  2025cites this paper
• Integer Reasoning Modulo Different Constants in SMT

  2025cites this paper
• ZK-ProVer: Proving Programming Verification in Non-Interactive Zero-Knowledge Proofs

  2025cites this paper
• Parallel Assembly Synthesis

  2024cites this paper
• ESBMC-Python: A Bounded Model Checker for Python Programs

  2024cites this paper
• Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration

  2024cites this paper
• Constraint solver selection based on the transformer model

  2024cites this paper
• ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST

  2024cites this paper
• Counterexample Guided Neural Network Quantization Refinement

  2024cites this paper
• Learning Branching-Time Properties in CTL and ATL via Constraint Solving

  2024cites this paper
• Improving Bit-Blasting for Nonlinear Integer Constraints

  2023cites this paper
• Automated Verification of Correctness for Masked Arithmetic Programs

  2023cites this paper
• A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification

  2023cites this paper
• Recurrent neural network implementation of digital integrated circuits to mitigate challenges in design verification

  2023cites this paper
• An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes

  2023cites this paper
• ESBMC v7.3: Model Checking C++ Programs using Clang AST

  2023cites this paper
• A Modeling Concept for Formal Verification of OS-Based Compositional Software

  2023cites this paper
• Simplifying Mixed Boolean-Arithmetic Obfuscation by Program Synthesis and Term Rewriting

  2023cites this paper
• Modelling and Verification of Security-Oriented Resource Partitioning Schemes

  2023cites this paper
• Grisette: Symbolic Compilation as a Functional Programming Library

  2023influential citation
• Transforming Numerical Feature Models into Propositional Formulas and the Universal Variability Language

  2023cites this paper
• Lightweight Online Learning for Sets of Related Problems in Automated Reasoning

  2023cites this paper
• Optimal Refinement-based Array Constraint Solving for Symbolic Execution

  2022cites this paper
• Kex at the 2022 SBST Tool Competition

  2022cites this paper
• Towards Porting Operating Systems with Program Synthesis

  2022cites this paper
• Variational satisfiability solving: efficiently solving lots of related SAT problems

  2022influential citation
• C for Yourself: Comparison of Front-End Techniques for Formal Verification

  2022influential citation
• Nemo: A Tool to Transform Feature Models with Numerical Features and Arithmetic Constraints

  2022cites this paper
• An HDL Simulator with Direct Register Access for Improving Code Coverage

  2022cites this paper
• A Comparison of SAT-based and SMT-based Frameworks for X-value Combinational Equivalence Checking

  2022cites this paper
• BFF: foundational and automated verification of bitfield-manipulating programs

  2022cites this paper
• An In-Place Simplification on Mixed Boolean-Arithmetic Expressions

  2022influential citation
• Overview I ’ m working on building algorithms and software for counting over SMT constraints with Dr

  2022cites this paper
• Reusing Solutions Modulo Theories

  2021cites this paper
• Satisfiability Modulo Theories

  2021cites this paper
• Towards a Formal Modelling, Analysis, and Verification of a Clone Node Attack Detection Scheme in the Internet of Things

  2021cites this paper
• Exploring Lifted Planning Encodings in Essence Prime

  2021cites this paper
• ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts

  2021cites this paper
• Generative type-aware mutation for testing SMT solvers

  2021cites this paper
• Vivienne: Relational Verification of Cryptographic Implementations in WebAssembly

  2021cites this paper
• Exploratory Review of Hybrid Fuzzing for Automated Vulnerability Detection

  2021cites this paper
• Inter‐cloud secure data sharing and its formal verification

  2021cites this paper
• Kex at the 2021 SBST Tool Competition

  2021cites this paper
• RANE: An Open-Source Formal De-obfuscation Attack for Reverse Engineering of Logic Encrypted Circuits

  2021influential citation
• A formally verified blockchain-based decentralised authentication scheme for the internet of things

  2021cites this paper
• A conflicts’ classification for IoT-based services: a comparative survey

  2021cites this paper
• On the Effect of the Key-expansion Algorithm in Simon-like Ciphers

  2021cites this paper
• Partial Specifications of Libraries: Applications in Software Engineering

  2021cites this paper
• Verifying Quantized Neural Networks using SMT-Based Model Checking

  2021cites this paper
• Integrated Reasoning Engine for Pointer-related Code Clone Detection

  2021cites this paper
• Porcupine: a synthesizing compiler for vectorized homomorphic encryption

  2021cites this paper
• Analysis and Transformation of Constrained Horn Clauses for Program Verification

  2021cites this paper
• STP models of optimal differential and linear trail for S-box based ciphers

  2021cites this paper
• Boosting SMT solver performance on mixed-bitwise-arithmetic expressions

  2021cites this paper
• Type and interval aware array constraint solving for symbolic execution

  2021influential citation
• SAT Competition 2020

  2021cites this paper
• Model checking C++ programs

  2021cites this paper
• KLEE symbolic execution engine in 2019

  2020cites this paper
• A Systematic Review of Search Strategies in Dynamic Symbolic Execution

  2020cites this paper
• Decision Procedures

  2020cites this paper
• SMT-based cube attack on round-reduced Simeck32/64

  2020cites this paper
• An Easy-to-Use Tool for Rotational-XOR Cryptanalysis of ARX Block Ciphers

  2020cites this paper
• ESBMC 6.1: automated test case generation using bounded model checking

  2020cites this paper
• Validating SMT solvers via semantic fusion

  2020cites this paper
• SMT Solver-Based Cryptanalysis of Block Ciphers

  2020cites this paper
• An Efficient Floating-Point Bit-Blasting API for Verifying C Programs

  2020cites this paper
• Recognition and Exploitation of Gate Structure in SAT Solving

  2020cites this paper
• Verification Runtime Analysis: Get the Most Out of Partial Verification

  2020cites this paper
• Map2Check: Using Symbolic Execution and Fuzzing

  2020cites this paper
• It Doesn’t Have to Be So Hard: Efficient Symbolic Reasoning for CRCs

  2020cites this paper
• Utilizing parametric systems for detection of pipeline hazards

  2020cites this paper
• Detecting critical bugs in SMT solvers using blackbox mutational fuzzing

  2020cites this paper
• Formal verification to ensuring the memory safety of C++ Programs

  2020cites this paper
• Satune: synthesizing efficient SAT encoders

  2020cites this paper
• Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison

  2020cites this paper
• Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning

  2020cites this paper
• L’usage de l’exécution symbolique pour la déobfuscation binaire en milieu industriel

  2020cites this paper
• A formal methods-based Rule Verification Framework for end-user programming in campus Building Automation Systems

  2020cites this paper
• Concurrent Bug Finding Based on Bounded Model Checking

  2020cites this paper
• Unifying Compilers for SNARKs, SMT, and More

  2020cites this paper
• Bit-Exact ECC Recovery (BEER): Determining DRAM On-Die ECC Functions by Exploiting DRAM Data Retention Characteristics

  2020cites this paper
• On the unusual effectiveness of type-aware operator mutations for testing SMT solvers

  2020cites this paper
• SymJEx: symbolic execution on the GraalVM

  2020cites this paper
• An SMT Theory of Fixed-Point Arithmetic

  2020influential citation
• Concurrent Bug Finding Based on Bounded Model Checking

  2020cites this paper
• Sys: A Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code

  2020cites this paper
• Reasoning about software security via synthesized behavioral substitutes

  2020cites this paper
• A Synthesis-Aided Compiler for DSP Architectures (WiP Paper)

  2020cites this paper
• Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers

  2019cites this paper
• Automatic Loop Summarization via Path Dependency Analysis

  2019cites this paper
• Theory Combination: Beyond Equality Sharing

  2019cites this paper
• Verifying fragility in digital systems with uncertainties using DSVerifier v2.0

  2019cites this paper
• Enhancing Symbolic Execution by Machine Learning Based Solver Selection

  2019influential citation