Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking. - Daisuke Ishii; Saito Fujii (TASE, 2020)