Masahiro Masuda, Yukiyoshi Kameyama: Program generation meets program verification: A case study on number-theoretic transform. Sci. Comput. Program. 232: 103035 (2024)