Please note: This is a beta version of the new dblp website.
You can find the classic dblp view of this page here.
You can find the classic dblp view of this page here.
David M. Russinoff
2010 – today
- 2013
[j8]David M. Russinoff: Computation and Formal Verification of SRT Quotient and Square Root Digit Selection Tables. IEEE Trans. Computers 62(5): 900-913 (2013)
2000 – 2009
- 2007
- [c2]
- 2000
- [c1]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
1990 – 1999
- 1999
- [j7]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
- [j6]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
- [j5]David M. Russinoff: A Mechanically Verified Incremental Garbage Collector. Formal Asp. Comput. 6(4): 359-390 (1994)
- 1992
- [j4]David M. Russinoff: A Verification System for Current Programs Based on the Boyer-Moore Prover. Formal Asp. Comput. 4(6A): 597-611 (1992)
- [j3]David M. Russinoff: A Mechanical Proof of Quadratic Reciprocity. J. Autom. Reasoning 8(1): 3-21 (1992)
- [j2]David M. Russinoff: A Verified Prolog Compiler for the Warren Abstract Machine. J. Log. Program. 13(4): 367-412 (1992)
1980 – 1989
- 1989
- [p1]David M. Russinoff: Proteus: A Frame-Based Nonmonotonic Inference System. Object-Oriented Concepts, Databases, and Applications 1989: 127-150
- 1985
- [j1]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)
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-04-11 18:40 CEST by the dblp team