David M. Russinoff - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 16 from 16

2022

Formal Verification of Floating-Point Hardware Design - A Mathematical Approach, Second EditionDavid M. Russinoff. Springer, 2022. [doi]

Formal Verification of a Chained Multiply-Add Design: Combining Theorem Proving and Equivalence CheckingDavid M. Russinoff, Javier Bruguera, Cuong Chau, Mayank Manjrekar, Nicholas Pfister, Harsha Valsaraju. arith 2022: 120-126 [doi]

2013

Computation and Formal Verification of SRT Quotient and Square Root Digit Selection TablesDavid M. Russinoff. TC, 62(5):900-913, 2013. [doi]

2010

A Mechanically Verified Commercial SRT DividerDavid M. Russinoff. In David S. Hardin, editor, Design and Verification of Microprocessor Systems for High-Assurance Applications. pages 23-63, Springer, 2010. [doi]

2007

A Mathematical Approach to RTL VerificationDavid M. Russinoff. cav 2007: 2 [doi]

2000

A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon:::TM::: ProcessorDavid M. Russinoff. FMCAD 2000: 3-36 [doi]

1999

A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root MicrocodeDavid M. Russinoff. fmsd, 14(1):75-125, 1999.

1998

™ ProcessorDavid M. Russinoff. lmsjcm, 1:148-200, 1998. [doi]

1995

A Formalization of a Subset of VHDL in the Boyer-Moore LogicDavid M. Russinoff. fmsd, 7(1/2):7-25, 1995.

1994

A Mechanically Verified Incremental Garbage CollectorDavid M. Russinoff. fac, 6(4):359-390, 1994.

1993

Specification and verification of gate-level VHDL models of synchronous and asynchronous circuitsDavid M. Russinoff. In Egon Börger, editor, Specification and validation methods. pages 411-460, Oxford University Press, 1993.

1992

A Mechanical Proof of Quadratic ReciprocityDavid M. Russinoff. JAR, 8(1):3-21, 1992.

A Verified Prolog Compiler for the Warren Abstract MachineDavid M. Russinoff. jlp, 13(4):367-412, 1992.

A Verification System for Current Programs Based on the Boyer-Moore ProverDavid M. Russinoff. fac, 4(6A):597-611, 1992.

1989

Proteus: A Frame-Based Nonmonotonic Inference SystemDavid M. Russinoff. In Object-Oriented Concepts, Databases, and Applications. pages 127-150, 1989.

1985

An Experiment with the Boyer-Moore Theorem Prover: A Proof of Wilson s TheoremDavid M. Russinoff. JAR, 1(2):121-139, 1985.

Sign in or sign up to see more results.

runs on WebDSL