Chocolat/SMV: A Translator from CafeOBJ into SMV
Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura, Kokichi Futatsugi · 2005
Chocolat/SMV is a translator that takes a CafeOBJ specification of a transition system called an OTS and generates an SMV specification of a finite version of the OTS. The primary purpose of the translation is to find errors lurked in CafeOBJ specifications of OTSs with SMV.