Summary

2020

Session Number:E03

Session:

Number:E03-3

Formal Verification and Code-Generation of Mersenne-Twister Algorithm

Takafumi Saikawa,  Kazunari Tanaka,  Kensaku Tanaka,  

pp.607-611

Publication Date:2020/10/18

Online ISSN:2188-5079

DOI:10.34385/proc.65.E03-3

PDF download

PayPerView

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 .