8 citations · 19 across the 7 of their papers we have counts for
7 papers
A Formalization of Finite Group Theory: Part II
David M. Russinoff
This is the second installment of an exposition of an ACL2 formalization of finite group theory. The first, which was presented at the 2022 ACL2 workshop, covered groups and subgro…
A Formalization of Finite Group Theory: Part III
David M. Russinoff
This is the third and final installment of an exposition of an ACL2 formalization of finite group theory. Part I covers groups and subgroups, cosets, normal subgroups, and quotient…
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…
Modeling Algorithms in SystemC and ACL2
John W. O'Leary, David M. Russinoff
We describe the formal language MASC, based on a subset of SystemC and intended for modeling algorithms to be implemented in hardware. By means of a special-purpose parser, an algo…