Model Checking (SMV)

Citation: Giuseppe Del Castillo and Kirsten Winter, "Model Checking Support for the ASM High-Level Language". Proceedings of 6th Int. Conference TACAS 2000, S. Graf, M. Schwartzbach (eds.), LNCS 1785, pp. 331-346, Springer-Verlag, 2000.
Summary: The authors introduce an interface from the ASM Workbench to the SMV model checking tool, based on an ASM-to-SMV transformation.
Subjects: Mechanical Verification
Download: Available from Kirsten Winter's home page in compressed PostScript.
Notes: An early version appeared as Universität-GH Paderborn Technical Report TR-RI-99-209. See also the paper on ASM Workbench, as well as an extension to the FLASH cache coherency protocol. Included in Winter's Ph.D. thesis.