David M. Russinoff

24 papers A* 1B 1C 1Journal 9Unranked 8

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	A Formalization of Elementary Linear Algebra: Part I. ACL2 David M. Russinoff
2023	—	`conf`	A Formalization of Finite Group Theory: Part II. ACL2 David M. Russinoff
2023	—	`conf`	A Formalization of Finite Group Theory: Part III. ACL2 David M. Russinoff
2022	—	`conf`	A Formalization of Finite Group Theory. ACL2 David M. Russinoff
2022	—	`book`	Formal Verification of Floating-Point Hardware Design - A Mathematical Approach, Second Edition Formal Verification of Floating-Point Hardware Design, 2nd Edition David M. Russinoff
2022	C	`conf`	Formal Verification of a Chained Multiply-Add Design: Combining Theorem Proving and Equivalence Checking. ARITH David M. Russinoff, Javier D. Bruguera, Cuong Chau, Mayank Manjrekar, Nicholas Pfister, Harsha Valsaraju
2022	—	`conf`	Properties of the Hebrew Calendar. ACL2 David M. Russinoff
2020	—	`conf`	Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2. ACL2 David M. Russinoff
2017	—	`conf`	A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve. ACL2 David M. Russinoff
2014	—	`conf`	Modeling Algorithms in SystemC and ACL2. ACL2 John W. O'Leary, David M. Russinoff
2013	J	`jnl`	Computation and Formal Verification of SRT Quotient and Square Root Digit Selection Tables. IEEE Trans. Computers David M. Russinoff
2010	—	`ch.`	A Mechanically Verified Commercial SRT Divider. Design and Verification of Microprocessor Systems for High-Assurance Applications David M. Russinoff
2007	A*	`conf`	A Mathematical Approach to RTL Verification. CAV David M. Russinoff
2000	B	`conf`	A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon FMCAD David M. Russinoff
1999	J	`jnl`	A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode. Formal Methods Syst. Des. David M. Russinoff
1998	J	`jnl`	A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7 LMS J. Comput. Math. David M. Russinoff
1995	J	`jnl`	A Formalization of a Subset of VHDL in the Boyer-Moore Logic. Formal Methods Syst. Des. David M. Russinoff
1994	J	`jnl`	A Mechanically Verified Incremental Garbage Collector. Formal Aspects Comput. David M. Russinoff
1993	—	`ch.`	Specification and verification of gate-level VHDL models of synchronous and asynchronous circuits. Specification and validation methods David M. Russinoff
1992	J	`jnl`	A Mechanical Proof of Quadratic Reciprocity. J. Autom. Reason. David M. Russinoff
1992	J	`jnl`	A Verification System for Current Programs Based on the Boyer-Moore Prover. Formal Aspects Comput. David M. Russinoff
1992	J	`jnl`	A Verified Prolog Compiler for the Warren Abstract Machine. J. Log. Program. David M. Russinoff
1989	—	`ch.`	Proteus: A Frame-Based Nonmonotonic Inference System. Object-Oriented Concepts, Databases, and Applications David M. Russinoff
1985	J	`jnl`	An Experiment with the Boyer-Moore Theorem Prover: A Proof of Wilson's Theorem. J. Autom. Reason. David M. Russinoff