On the public citation graph

Using an induction prover for verifying arithmetic circuits

https://doi.org/10.1007/pl00010808
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/0-387-97226-9_34openalex-snapshot
The verification of a bit-slice ALU
inferredcites →https://doi.org/10.1007/3-540-49366-2_3openalex-snapshot
Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover
inferredcites →https://doi.org/10.1007/3-540-55602-8_173openalex-snapshot
Difference matching
inferredcites →https://doi.org/10.1007/3-540-56393-8_28openalex-snapshot
Implementing contextual rewriting
inferredcites →https://doi.org/10.1007/3-540-58156-1_2openalex-snapshot
A divergence critic
inferredcites →https://doi.org/10.1007/3-540-59047-1_50openalex-snapshot
Effective theorem proving for hardware verification
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/3-540-61474-5_64openalex-snapshot
Mechanically verifying a family of multiplier circuits
inferredcites →https://doi.org/10.1007/3-540-61511-3_112openalex-snapshot
Lemma discovery in automating induction
inferredcites →https://doi.org/10.1007/3-540-62950-5_59openalex-snapshot
Shostak's congruence closure as completion
inferredcites →https://doi.org/10.1007/bf00244460openalex-snapshot
Productive use of failure in inductive proof
inferredcites →https://doi.org/10.1007/bfb0012831openalex-snapshot
A mechanizable induction principle for equational specifications
inferredcites →https://doi.org/10.1007/bfb0013060openalex-snapshot
The use of planning critics in mechanizing inductive proofs
inferredcites →https://doi.org/10.1007/bfb0028393openalex-snapshot
Rewriting, decision procedures and lemma speculation for automated hardware verification
inferredcites →https://doi.org/10.1007/bfb0031800openalex-snapshot
Verification of IEEE compliant subtractive division algorithms
inferredcites →https://doi.org/10.1016/0378-4754(89)90181-xopenalex-snapshot
A computational logic handbook
inferredcites →https://doi.org/10.1016/0898-1221(94)00218-aopenalex-snapshot
An overview of Rewrite Rule Laboratory (RRL)
inferredcites →https://doi.org/10.1016/b978-0-444-89208-9.50008-9openalex-snapshot
A METHODOLOGY FOR PROVING CORRECTNESS OF PARAMETERIZED HARDWARE MODULES IN HOL
inferredcites →https://doi.org/10.1016/s0747-7171(87)80022-6openalex-snapshot
Termination of rewriting
inferredcites →https://doi.org/10.1017/cbo9780511569845.004openalex-snapshot
Hardware Verification using Higher Order Logic
inferredcites →https://doi.org/10.1057/jors.1991.155openalex-snapshot
Introduction to Algorithms
inferredcites →https://doi.org/10.1093/qjmam/11.3.364openalex-snapshot
TECHNIQUES OF MULTIPLICATION AND DIVISION FOR AUTOMATIC BINARY COMPUTERS
inferredcites →https://doi.org/10.1109/12.57040openalex-snapshot
Radix-4 square rot without initial PLA
inferredcites →https://doi.org/10.1109/arith.1981.6159293openalex-snapshot
Compatible hardware for division and square root
inferredcites →https://doi.org/10.1109/arith.1993.378104openalex-snapshot
Measuring the accuracy of ROM reciprocal tables
inferredcites →https://doi.org/10.1109/pgec.1964.263830openalex-snapshot
A Suggestion for a Fast Multiplier
inferredcites →https://doi.org/10.1109/tc.1986.1676819openalex-snapshot
Graph-Based Algorithms for Boolean Function Manipulation
inferredcites →https://doi.org/10.1109/tc.1987.5009445openalex-snapshot
Design of a Hih-Speed Square Root Multiply and Divide Unit
inferredcites →https://doi.org/10.1109/tec.1958.5222579openalex-snapshot
A New Class of Digital Division Methods
inferredcites →https://doi.org/10.1145/123186.123223openalex-snapshot
Sequential circuit verification using symbolic model checking
inferredcites →https://doi.org/10.1145/240518.240643openalex-snapshot
Bit-level analysis of an SRT divider circuit
inferredcites →https://doi.org/10.1145/2422.322411openalex-snapshot
Deciding Combinations of Theories
inferredcites →https://doi.org/10.1145/357073.357079openalex-snapshot
Simplification by Cooperating Decision Procedures
inferredcites →https://doi.org/10.1147/rd.341.0059openalex-snapshot
Design of the IBM RISC System/6000 floating-point execution unit
inferredcites →https://doi.org/10.21236/ada281028openalex-snapshot
Verification of Arithmetic Functions with Binary Moment Diagrams

What points at this work

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

inferred← citeshttps://doi.org/10.1006/ijhc.2002.1007openalex-snapshot
KJ3—a tool assisting formal validation of knowledge-based systems
inferred← citeshttps://doi.org/10.1007/10721959_26openalex-snapshot
Extending Decision Procedures with Induction Schemes
inferred← citeshttps://doi.org/10.1007/3-540-45988-x_8openalex-snapshot
A Rewrite Rule Based Framework for Combining Decision Procedures *
inferred← citeshttps://doi.org/10.1007/978-1-4615-1391-9_8openalex-snapshot
On the Construction of a Domain Language for a Class of Reactive Systems
inferred← citeshttps://doi.org/10.1007/978-3-540-25984-8_13openalex-snapshot
argo-lib: A Generic Platform for Decision Procedures
inferred← citeshttps://doi.org/10.1007/978-3-540-40965-6_9openalex-snapshot
Automatic Generation of Simple Lemmas from Recursive Definitions Using Decision Procedures – Preliminary Report –
inferred← citeshttps://doi.org/10.1007/978-3-7091-6280-4_13openalex-snapshot
Rewriting, Induction and Decision Procedures: A Case Study of Presburger Arithmetic
inferred← citeshttps://doi.org/10.1007/pl00010806openalex-snapshot
Theorem proving in technology transfer: the user’s point of view
inferred← citeshttps://doi.org/10.1023/a:1015707001763openalex-snapshot
A General Setting for Flexibly Combining and Augmenting Decision Procedures
inferred← citeshttps://doi.org/10.1109/date.2002.998245openalex-snapshot
Formal verification of the Pentium/sup /spl reg//4 floating-point multiplier
inferred← citeshttps://doi.org/10.1109/fpl.2005.1515694openalex-snapshot
Felix: using rewriting-logic for generating functionally equivalent implementations
inferred← citeshttps://doi.org/10.1109/fpl.2006.311289openalex-snapshot
From Equation to VHDL: Using Rewriting Logic for Automated Function Generation
inferred← citeshttps://doi.org/10.1109/ipdps.2007.370369openalex-snapshot
Using Rewriting Logic to Match Patterns of Instructions from a Compiler Intermediate Form to Coarse-Grained Processing Elements
inferred← citeshttps://doi.org/10.1109/sbcci.2003.1232830openalex-snapshot
Modeling a reconfigurable system for computing the FFT in place via rewriting-logic
inferred← citeshttps://doi.org/10.1109/sccc.2003.1245446openalex-snapshot
Efficient computation of algebraic operations over dynamically reconfigurable systems specified by rewriting-logic environments
inferred← citeshttps://doi.org/10.1109/vlsid.2014.21openalex-snapshot
Formal Verification and Debugging of Array Dividers with Auto-correction Mechanism
inferred← citeshttps://doi.org/10.1145/1016568.1016634openalex-snapshot
Modeling and prototyping dynamically reconfigurable systems for efficient computation of dynamic programming methods by rewriting-logic
inferred← citeshttps://doi.org/10.1145/1142155.1142156openalex-snapshot
Prototyping time- and space-efficient computations of algebraic operations over dynamically reconfigurable systems modeled by rewriting-logic
inferred← citeshttps://doi.org/10.1145/1150343.1150379openalex-snapshot
SAEPTUM
inferred← citeshttps://doi.org/10.1145/2660540.2660982openalex-snapshot
Verification of Hardware Implementations through Correctness of their Recursive Definitions in PVS
inferred← citeshttps://doi.org/10.1145/3649329.3657311openalex-snapshot
Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once
inferred← citeshttps://doi.org/10.5555/882452.874523openalex-snapshot
Formal Verification of the Pentium® 4 Floating-Point Multiplier
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.