www.prismmodelchecker.org
[MP19] P. Milazzo and G. Pardini. Objective/MC: A high-level model checking language. Journal of Intelligent Information Systems volume, 52, pages 533–571. 2019. [Presents a high-level imperative modelling language and a translation into PRISM.]
Links: [Google] [Google Scholar]

Publications