On the public citation graph

Interactive Bitvector Reasoning using Verified Bit-Blasting

https://doi.org/10.1145/3763167
0 signed · 58 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.
Claim with ORCID
Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/978-3-030-81688-9_7openalex-snapshot
CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver
inferredcites →https://doi.org/10.1007/978-3-030-99524-9_24openalex-snapshot
cvc5: A Versatile and Industrial-Strength SMT Solver
inferredcites →https://doi.org/10.1007/978-3-031-37703-7_1openalex-snapshot
Bitwuzla
inferredcites →https://doi.org/10.1007/978-3-031-65627-9_7openalex-snapshot
CaDiCaL 2.0
inferredcites →https://doi.org/10.1007/978-3-319-08867-9_45openalex-snapshot
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors
inferredcites →https://doi.org/10.1007/978-3-319-63046-5_14openalex-snapshot
Efficient Certified RAT Verification
inferredcites →https://doi.org/10.1007/978-3-319-63390-9_7openalex-snapshot
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
inferredcites →https://doi.org/10.1007/978-3-319-66263-3_29openalex-snapshot
The GRAT Tool Chain
inferredcites →https://doi.org/10.1007/978-3-540-71067-7_7openalex-snapshot
The Isabelle Framework
inferredcites →https://doi.org/10.1007/978-3-540-73368-3_52openalex-snapshot
A Decision Procedure for Bit-Vectors and Arrays
inferredcites →https://doi.org/10.1007/978-3-540-78800-3_24openalex-snapshot
Z3: An Efficient SMT Solver
inferredcites →https://doi.org/10.1007/978-3-642-00768-2_16openalex-snapshot
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays
inferredcites →https://doi.org/10.1007/978-3-642-02658-4_53openalex-snapshot
Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
inferredcites →https://doi.org/10.1007/978-3-642-14052-5_11openalex-snapshot
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
inferredcites →https://doi.org/10.1007/978-3-642-14203-1_9openalex-snapshot
Sledgehammer: Judgement Day
inferredcites →https://doi.org/10.1007/978-3-642-22110-1_14openalex-snapshot
CVC4
inferredcites →https://doi.org/10.1007/978-3-642-24364-6_2openalex-snapshot
Automatic Proof and Disproof in Isabelle/HOL
inferredcites →https://doi.org/10.1007/978-3-642-24690-6_28openalex-snapshot
The Boogie Verification Debugger (Tool Paper)
inferredcites →https://doi.org/10.1007/978-3-642-25379-9_15openalex-snapshot
Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
inferredcites →https://doi.org/10.1007/978-3-642-37036-6_8openalex-snapshot
Why3 — Where Programs Meet Provers
inferredcites →https://doi.org/10.1007/978-3-642-81955-1_28openalex-snapshot
On the Complexity of Derivation in Propositional Calculus
inferredcites →https://doi.org/10.1007/bfb0031814openalex-snapshot
HOL Light: A tutorial introduction
inferredcites →https://doi.org/10.1007/s10703-012-0163-3openalex-snapshot
SMT proof checking using a logical framework
inferredcites →https://doi.org/10.1109/arith.2011.40openalex-snapshot
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq
inferredcites →https://doi.org/10.1109/arith.2013.30openalex-snapshot
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
inferredcites →https://doi.org/10.1109/cgo.2004.1281665openalex-snapshot
LLVM: a compilation framework for lifelong program analysis & transformation
inferredcites →https://doi.org/10.1109/cmpass.1996.507872openalex-snapshot
ACL2: an industrial strength version of Nqthm
inferredcites →https://doi.org/10.1109/fmcad.2016.7886675openalex-snapshot
Trustworthy specifications of ARM® v8-A and v8-M system level architecture
inferredcites →https://doi.org/10.1145/1476589.1476628openalex-snapshot
Response time in man-computer conversational transactions
inferredcites →https://doi.org/10.1145/1670412openalex-snapshot
Proceedings of the 7th International Workshop on Satisfiability Modulo Theories
inferredcites →https://doi.org/10.1145/2103656.2103709openalex-snapshot
Formalizing the LLVM intermediate representation for verified program transformations
inferredcites →https://doi.org/10.1145/277044.277186openalex-snapshot
A decision procedure for bit-vector arithmetic
inferredcites →https://doi.org/10.1145/3133956.3134043openalex-snapshot
HACL*: A Verified Modern Cryptographic Library
inferredcites →https://doi.org/10.1145/3290384openalex-snapshot
ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS
inferredcites →https://doi.org/10.1145/3372885.3373824openalex-snapshot
The lean mathematical library
inferredcites →https://doi.org/10.1145/3385412.3385965openalex-snapshot
The essence of Bluespec: a core language for rule-based hardware design
inferredcites →https://doi.org/10.1145/3408997openalex-snapshot
Sealing pointer-based optimizations behind pure functions
inferredcites →https://doi.org/10.1145/3412932.3412935openalex-snapshot
Counting immutable beans
inferredcites →https://doi.org/10.1145/3453483.3454030openalex-snapshot
Alive2: bounded translation validation for LLVM
inferredcites →https://doi.org/10.1145/3560810.3565290openalex-snapshot
Intel HERACLES
inferredcites →https://doi.org/10.1145/3605769.3623993openalex-snapshot
Enabling Lattice-Based Post-Quantum Cryptography on the OpenTitan Platform
inferredcites →https://doi.org/10.4204/eptcs.114.8openalex-snapshot
Verified AIG Algorithms in ACL2
inferredcites →https://doi.org/10.4204/eptcs.192.6openalex-snapshot
Extending ACL2 with SMT Solvers
inferredcites →https://doi.org/10.4204/eptcs.70.7openalex-snapshot
Bit-Blasting ACL2 Theorems
inferredcites →https://doi.org/10.4230/lipics.sat.2023.21openalex-snapshot
Faster LRAT Checking Than Solving with CaDiCaL
inferredcites →https://doi.org/10.48550/arxiv.2407.03685openalex-snapshot
Verifying Peephole Rewriting In SSA Compiler IRs
inferredcites →https://doi.org/10.5281/zenodo.15755236openalex-snapshot
Interactive Bit Vector Reasoning using Verified Bitblasting
inferredcites →https://doi.org/10.6092/issn.1972-5787/1979openalex-snapshot
An introduction to small scale reflection in Coq

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.5281/zenodo.23548859zenodo-depositor-declared
inferred← citeshttps://doi.org/10.5281/zenodo.23562432zenodo-depositor-declared
inferred← citeshttps://doi.org/10.5281/zenodo.23574724zenodo-depositor-declared
inferred← citeshttps://doi.org/10.5281/zenodo.23607175zenodo-depositor-declared
inferred← citeshttps://doi.org/10.5281/zenodo.23634505zenodo-depositor-declared
inferred← citeshttps://doi.org/10.5281/zenodo.23754649zenodo-depositor-declared
inferred← citeshttps://doi.org/10.5281/zenodo.23956571zenodo-depositor-declared
inferred← citeshttps://doi.org/10.1007/978-3-032-22752-2_13openalex-snapshot
Hint-Based SMT Proof Reconstruction
inferred← citeshttps://doi.org/10.1007/978-3-032-32526-6_8openalex-snapshot
Automating Bitvector and Finite Field Equivalence Proofs in Lean
inferred← citeshttps://doi.org/10.1145/3839511openalex-snapshot
Sound and Complete Solving for Multi-width Parametric Bitvectors via Principled Reductions
Editorial review for independent work. ICSAC — the Institute for Complexity Science and Advanced Computing — runs a structured editorial panel for researchers publishing outside journals, and publishes on CiteStamp rails. Submission is free and goes through ORCID: icsacinstitute.org/submit.