4 citations · 4 across the 3 of their papers we have counts for
4 papers
A Formalization of Finite Group Theory
David M. Russinoff
Previous formulations of group theory in ACL2 and Nqthm, based on either "encapsulate" or "defn-sk", have been limited by their failure to provide a path to proof by induction on t…
Properties of the Hebrew Calendar
David M. Russinoff
We describe an ACL2 program that implements the Hebrew calendar and the formal verification of several of its properties, including the critical result that the algorithm that dete…
Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2
David M. Russinoff
We present a methodology for formal verification of arithmetic RTL designs that combines sequential logic equivalence checking with interactive theorem proving. An intermediate mod…
A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve
David M. Russinoff
We present an elementary proof of the group properties of the elliptic curve known as "Curve25519", as a component of a comprehensive proof of correctness of a hardware implementat…