On the public citation graph

Verification of IEEE compliant subtractive division algorithms

https://doi.org/10.1007/bfb0031800
0 signed · 46 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/3-540-59047-1_42openalex-snapshot
Non-restoring integer square root: A case study in design by principled optimization
inferredcites →https://doi.org/10.1007/3-540-59293-8openalex-snapshot
TAPSOFT '95: Theory and Practice of Software Development
inferredcites →https://doi.org/10.1007/3-540-59293-8_189openalex-snapshot
Anatomy of the Pentium bug
inferredcites →https://doi.org/10.1007/3-540-60275-5_65openalex-snapshot
Floating point verification in HOL
inferredcites →https://doi.org/10.1007/3-540-61474-5_62openalex-snapshot
Verifying the SRT division algorithm using theorem proving techniques
inferredcites →https://doi.org/10.1007/3-540-61474-5_63openalex-snapshot
Modular verification of SRT division
inferredcites →https://doi.org/10.1007/bf01383955openalex-snapshot
A proof of the nonrestoring division algorithm and its implementation on an ALU
inferredcites →https://doi.org/10.1016/s1474-6670(17)44819-1openalex-snapshot
DRS - Derivational Reasoning System: A Digital Design Derivation System for Hardware Synthesis *
inferredcites →https://doi.org/10.1109/32.24710openalex-snapshot
Formal methods applied to a floating-point number system
inferredcites →https://doi.org/10.1109/32.345827openalex-snapshot
Formal verification for fault-tolerant architectures: prolegomena to the design of PVS
inferredcites →https://doi.org/10.1109/arith.1981.6159293openalex-snapshot
Compatible hardware for division and square root
inferredcites →https://doi.org/10.1109/arith.1987.6158683openalex-snapshot
A formal approach to rounding
inferredcites →https://doi.org/10.1109/iccad.1995.479878openalex-snapshot
The formal verification of a pipelined double-precision IEEE floating-point multiplier
inferredcites →https://doi.org/10.1109/iccd.1995.528918openalex-snapshot
Verification of a subtractive radix-2 square root algorithm and implementation
inferredcites →https://doi.org/10.1145/1478786.1478840openalex-snapshot
A unified algorithm for elementary functions
inferredcites →https://doi.org/10.1201/9781315275567openalex-snapshot
Computer Arithmetic Algorithms
inferredcites →https://doi.org/10.25291/vr/1987-vr-854openalex-snapshot
PRACTICE NOTE No 2 of 1987
inferredcites →https://doi.org/10.5555/224841.224851openalex-snapshot
The formal verification of a pipelined double-precision IEEE floating-point multiplier

What points at this work

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

inferred← citeshttps://doi.org/10.1007/3-540-44798-9_26openalex-snapshot
Formal Verification of the VAMP Floating Point Unit
inferred← citeshttps://doi.org/10.1007/3-540-47884-1_11openalex-snapshot
Formalization of Cadence SPW Fixed-Point Arithmetic in HOL
inferred← citeshttps://doi.org/10.1007/3-540-48119-2_26openalex-snapshot
Structural Embeddings: Mechanization with Method
inferred← citeshttps://doi.org/10.1007/3-540-48257-1_24openalex-snapshot
PVS: An Experience Report
inferred← citeshttps://doi.org/10.1007/3-540-49366-2_3openalex-snapshot
Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover
inferred← citeshttps://doi.org/10.1007/3-540-62034-6_36openalex-snapshot
Mechanized formal methods: Progress and prospects
inferred← citeshttps://doi.org/10.1007/978-0-387-35190-2_17openalex-snapshot
Integrated Reasoning Support in System Design: Design Derivation and Theorem Proving
inferred← citeshttps://doi.org/10.1007/978-3-540-39724-3_29openalex-snapshot
Linear and Nonlinear Arithmetic in ACL2
inferred← citeshttps://doi.org/10.1007/978-3-540-39893-6_13openalex-snapshot
Modeling SystemC Fixed-Point Arithmetic in HOL
inferred← citeshttps://doi.org/10.1007/978-3-642-60858-2_26openalex-snapshot
Machine-Assisted Verification Using Theorem Proving and Model Checking
inferred← citeshttps://doi.org/10.1007/bfb0000475openalex-snapshot
Floating point verification in HOL light: The exponential function
inferred← citeshttps://doi.org/10.1007/bfb0031801openalex-snapshot
Hierarchical verification of two-dimensional high-speed multiplication in PVS: A case study
inferred← citeshttps://doi.org/10.1007/bfb0035400openalex-snapshot
Integration in PVS: Tables, types, and model checking
inferred← citeshttps://doi.org/10.1007/bfb0058026openalex-snapshot
Mechanizing verification of arithmetic circuits: SRT division
inferred← citeshttps://doi.org/10.1007/pl00010808openalex-snapshot
Using an induction prover for verifying arithmetic circuits
inferred← citeshttps://doi.org/10.1007/s10009-003-0120-yopenalex-snapshot
Properties of two’s complement floating point notations
inferred← citeshttps://doi.org/10.1007/s10703-005-1613-yopenalex-snapshot
Formal Verification of the VAMP Floating Point Unit
inferred← citeshttps://doi.org/10.1007/s10703-005-2256-8openalex-snapshot
Formalization of Fixed-Point Arithmetic in HOL
inferred← citeshttps://doi.org/10.1007/s10836-024-06123-9openalex-snapshot
Formal Verification of Universal Numbers using Theorem Proving
inferred← citeshttps://doi.org/10.1023/a:1008617612073openalex-snapshot
Modular Verification of SRT Division
inferred← citeshttps://doi.org/10.1023/a:1008669628911openalex-snapshot
A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode
inferred← citeshttps://doi.org/10.1023/a:1008712907154openalex-snapshot
Floating Point Verification in HOL Light: The Exponential Function
inferred← citeshttps://doi.org/10.1093/comjnl/bxp023openalex-snapshot
Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL
inferred← citeshttps://doi.org/10.1109/12.713311openalex-snapshot
A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
inferred← citeshttps://doi.org/10.1109/cmpass.1995.521893openalex-snapshot
NASA Langley's research and technology-transfer program in formal methods
inferred← citeshttps://doi.org/10.1145/1141277.1141586openalex-snapshot
Provably faithful evaluation of polynomials
inferred← citeshttps://doi.org/10.1145/307988.307989openalex-snapshot
Formal verification in hardware design
inferred← citeshttps://doi.org/10.22028/d291-25704openalex-snapshot
Formal verification of a fully IEEE compliant floating point unit
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.