 | 2007 |
|---|
| 10 |       | David M. Russinoff:
A Mathematical Approach to RTL Verification.
CAV 2007: 2 |
| 2000 |
|---|
| 9 | | David M. Russinoff:
A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD AthlonTM Processor.
FMCAD 2000: 3-36 |
| 1999 |
|---|
| 8 |  | David M. Russinoff:
A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode.
Formal Methods in System Design 14(1): 75-125 (1999) |
| 1995 |
|---|
| 7 | | David M. Russinoff:
A Formalization of a Subset of VHDL in the Boyer-Moore Logic.
Formal Methods in System Design 7(1/2): 7-25 (1995) |
| 1994 |
|---|
| 6 | | David M. Russinoff:
A Mechanically Verified Incremental Garbage Collector.
Formal Asp. Comput. 6(4): 359-390 (1994) |
| 1992 |
|---|
| 5 | | David M. Russinoff:
A Verification System for Current Programs Based on the Boyer-Moore Prover.
Formal Asp. Comput. 4(6A): 597-611 (1992) |
| 4 | | David M. Russinoff:
A Mechanical Proof of Quadratic Reciprocity.
J. Autom. Reasoning 8(1): 3-21 (1992) |
| 3 | | David M. Russinoff:
A Verified Prolog Compiler for the Warren Abstract Machine.
J. Log. Program. 13(4): 367-412 (1992) |
| 1989 |
|---|
| 2 | | David M. Russinoff:
Proteus: A Frame-Based Nonmonotonic Inference System.
Object-Oriented Concepts, Databases, and Applications 1989: 127-150 |
| 1985 |
|---|
| 1 | | David M. Russinoff:
An Experiment with the Boyer-Moore Theorem Prover: A Proof of Wilson's Theorem.
J. Autom. Reasoning 1(2): 121-139 (1985) |
