Objective/MC is a prototype high level model checking language. ObjMC is a compiler for the Objective/MC language, generating a DTMC PRISM model. It has been developed in C++, and is available under GPL license. The current version of the tool is: 0.12, released in 2016. The tool can be downloaded from the following web page: www.di.unipi.it/msvbio/ObjMC/ . The tool has been described and used in the following publication: Pardini, G., & Milazzo, P. (2016, July). A High-Level Model Checking Language with Compile-Time Pruning of Local Variables. In Federation of International Conferences on Software Technologies: Applications and Foundations. LNCS 9946, pp. 67-82, Springer International Publishing.
ObjMC: The Objective/MC compiler
MILAZZO, PAOLO;PARDINI, GIOVANNI
2016-01-01
Abstract
Objective/MC is a prototype high level model checking language. ObjMC is a compiler for the Objective/MC language, generating a DTMC PRISM model. It has been developed in C++, and is available under GPL license. The current version of the tool is: 0.12, released in 2016. The tool can be downloaded from the following web page: www.di.unipi.it/msvbio/ObjMC/ . The tool has been described and used in the following publication: Pardini, G., & Milazzo, P. (2016, July). A High-Level Model Checking Language with Compile-Time Pruning of Local Variables. In Federation of International Conferences on Software Technologies: Applications and Foundations. LNCS 9946, pp. 67-82, Springer International Publishing.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
