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) |