Formal Verification and Code-Generation of Mersenne-Twister Algorithm

摘要

We formalize the pseudocode and linear-algebraic presentations of Mersenne-Twister, and formally establish their equivalence. Based on this formalization, we investigate the long-period property of Mersenne-Twister, formally proving that the property is reduced to the primitivity of the characteristic polynomial of the matrix representation.The formalization is done in COQ proof assistant. This enables us to generate a C program code from the verified pseudocode written in COQ.