2007 |
10 | EE | David M. Russinoff:
A Mathematical Approach to RTL Verification.
CAV 2007: 2 |
2000 |
9 | EE | 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) |