David M. Russinoff

According to our database, David M. Russinoff authored at least 24 papers between 1985 and 2025.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2025

A Formalization of Elementary Linear Algebra: Part I.

David M. Russinoff

Proceedings of the Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications, July, 2025

2023

A Formalization of Finite Group Theory: Part II.

David M. Russinoff

Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, 2023

A Formalization of Finite Group Theory: Part III.

David M. Russinoff

Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, 2023

2022

A Formalization of Finite Group Theory.

David M. Russinoff

Proceedings of the Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, 2022

Properties of the Hebrew Calendar.

David M. Russinoff

Proceedings of the Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, 2022

Formal Verification of a Chained Multiply-Add Design: Combining Theorem Proving and Equivalence Checking.

David M. Russinoff, Javier D. Bruguera, Cuong Chau, Mayank Manjrekar, Nicholas Pfister, Harsha Valsaraju

Proceedings of the 29th IEEE Symposium on Computer Arithmetic, 2022

Formal Verification of Floating-Point Hardware Design - A Mathematical Approach, Second Edition

David M. Russinoff

Springer, ISBN: 978-3-030-87180-2, 2022

2020

Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2.

David M. Russinoff

Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, 2020

2017

A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve.

David M. Russinoff

Proceedings of the Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, 2017

2014

Modeling Algorithms in SystemC and ACL2.

John W. O'Leary, David M. Russinoff

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

2013

Computation and Formal Verification of SRT Quotient and Square Root Digit Selection Tables.

David M. Russinoff

IEEE Trans. Computers, 2013

2010

A Mechanically Verified Commercial SRT Divider.

David M. Russinoff

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2007

A Mathematical Approach to RTL Verification.

David M. Russinoff

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2000

A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon^TM Processor.

David M. Russinoff

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

1999

A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode.

David M. Russinoff

Formal Methods Syst. Des., 1999

1998

A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor.

David M. Russinoff

LMS J. Comput. Math., 1998

1995

A Formalization of a Subset of VHDL in the Boyer-Moore Logic.

David M. Russinoff

Formal Methods Syst. Des., 1995

1994

A Mechanically Verified Incremental Garbage Collector.

David M. Russinoff

Formal Aspects Comput., 1994

1993

Specification and verification of gate-level VHDL models of synchronous and asynchronous circuits.

David M. Russinoff

Proceedings of the Specification and validation methods, 1993

1992

A Verified Prolog Compiler for the Warren Abstract Machine.

David M. Russinoff

J. Log. Program., 1992

A Mechanical Proof of Quadratic Reciprocity.

David M. Russinoff

J. Autom. Reason., 1992

A Verification System for Current Programs Based on the Boyer-Moore Prover.

David M. Russinoff

Formal Aspects Comput., 1992

1989

Proteus: A Frame-Based Nonmonotonic Inference System.

David M. Russinoff

Proceedings of the Object-Oriented Concepts, Databases, and Applications., 1989

1985

An Experiment with the Boyer-Moore Theorem Prover: A Proof of Wilson's Theorem.

David M. Russinoff

J. Autom. Reason., 1985