Search the dblp DataBase

Publications of Author

1. David M. Russinoff
   A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon^TM Processor. [Citation Graph (0, 0)][DBLP]
   FMCAD, 2000, pp:3-36 [Conf]
   
2. David M. Russinoff
   A Verification System for Current Programs Based on the Boyer-Moore Prover. [Citation Graph (0, 0)][DBLP]
   Formal Asp. Comput., 1992, v:4, n:6A, pp:597-611 [Journal]
   
3. David M. Russinoff
   A Mechanically Verified Incremental Garbage Collector. [Citation Graph (0, 0)][DBLP]
   Formal Asp. Comput., 1994, v:6, n:4, pp:359-390 [Journal]
   
4. David M. Russinoff
   A Formalization of a Subset of VHDL in the Boyer-Moore Logic. [Citation Graph (0, 0)][DBLP]
   Formal Methods in System Design, 1995, v:7, n:1/2, pp:7-25 [Journal]
   
5. David M. Russinoff
   A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode. [Citation Graph (0, 0)][DBLP]
   Formal Methods in System Design, 1999, v:14, n:1, pp:75-125 [Journal]
   
6. David M. Russinoff
   An Experiment with the Boyer-Moore Theorem Prover: A Proof of Wilson's Theorem. [Citation Graph (0, 0)][DBLP]
   J. Autom. Reasoning, 1985, v:1, n:2, pp:121-139 [Journal]
   
7. David M. Russinoff
   A Mechanical Proof of Quadratic Reciprocity. [Citation Graph (0, 0)][DBLP]
   J. Autom. Reasoning, 1992, v:8, n:1, pp:3-21 [Journal]
   
8. David M. Russinoff
   A Verified Prolog Compiler for the Warren Abstract Machine. [Citation Graph (0, 0)][DBLP]
   J. Log. Program., 1992, v:13, n:4, pp:367-412 [Journal]
   
9. David M. Russinoff
   A Mathematical Approach to RTL Verification. [Citation Graph (0, 0)][DBLP]
   CAV, 2007, pp:2- [Conf]