{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T04:11:29Z","timestamp":1750824689579,"version":"3.41.0"},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,8,1]],"date-time":"2017-08-01T00:00:00Z","timestamp":1501545600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Intell Inf Syst"],"published-print":{"date-parts":[[2019,6]]},"DOI":"10.1007\/s10844-017-0475-2","type":"journal-article","created":{"date-parts":[[2017,8,1]],"date-time":"2017-08-01T07:41:45Z","timestamp":1501573305000},"page":"533-571","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Objective\/MC: A high-level model checking language"],"prefix":"10.1007","volume":"52","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7309-6424","authenticated-orcid":false,"given":"P.","family":"Milazzo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Pardini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,1]]},"reference":[{"key":"475_CR1","unstructured":"Abadi, M., & Cardelli, L. (2012). A theory of objects. Springer Science & Business Media."},{"key":"475_CR2","unstructured":"Cardelli, L. (2004). Type systems Tucker, A.B. (Ed.) Computer science handbook, 2nd Edn. Chapman and Hall\/CRC, chap. 97."},{"key":"475_CR3","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., & Tacchella, A. (2002). NuSMV 2: An opensource tool for symbolic model checking. In Computer aided verification (pp. 359\u2013364). Springer.","DOI":"10.1007\/3-540-45657-0_29"},{"key":"475_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., & Lerda, F. (2004). A tool for checking ANSI-C programs. In Tools and Alg. for the Construction and Analysis of Systems (pp. 168\u2013176). Springer.","DOI":"10.1007\/978-3-540-24730-2_15"},{"issue":"2","key":"475_CR5","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u0131-Oliet, N., Meseguer, J., & Quesada, J.F. (2002). Maude: specification and programming in rewriting logic. Theoretical Computer Science, 285(2), 187\u2013243.","journal-title":"Theoretical Computer Science"},{"key":"475_CR6","doi-asserted-by":"crossref","unstructured":"Habermaier, A., Leupolz, J., & Reif, W. (2016). Unified simulation, visualization, and formal analysis of safety-critical systems with. In International workshop on formal methods for industrial critical systems (pp. 150\u2013167). Springer.","DOI":"10.1007\/978-3-319-45943-1_11"},{"issue":"4","key":"475_CR7","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., & Pressburger, T. (2000). Model checking Java programs using Java Pathfinder. International Journal on Software Tools for Technology Transfer, 2(4), 366\u2013381.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"5","key":"475_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J. (1997). The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), 279.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"475_CR9","unstructured":"Kwiatkowska, M., Norman, G., & Parker, D. (2011). PRISM 4.0: Verification of probabilistic real-time systems. In Computer aided verification (pp. 585\u2013591). Springer."},{"issue":"1","key":"475_CR10","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., & Yi, W. (1997). UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer (STTT), 1(1), 134\u2013152.","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"475_CR11","unstructured":"ObjMC ver. 0.12 (2016). ObjMC: The Objective\/MC compiler. http:\/\/www.di.unipi.it\/msvbio\/ObjMC\/ ."},{"key":"475_CR12","unstructured":"Pardini, G., & Milazzo, P. (2016). A high-level model checking language with compile-time pruning of local variables. In Software technologies: applications and foundations, lecture notes in computer science (Vol. 9946, pp. 67\u201382). Springer."},{"issue":"4","key":"475_CR13","doi-asserted-by":"crossref","first-page":"385","DOI":"10.3233\/FUN-2004-63405","volume":"63","author":"M Sirjani","year":"2004","unstructured":"Sirjani, M., Movaghar, A., Shali, A., & De Boer, F.S. (2004). Modeling and verification of reactive systems using Rebeca. Fundamenta Informaticae, 63(4), 385\u2013410.","journal-title":"Fundamenta Informaticae"}],"container-title":["Journal of Intelligent Information Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10844-017-0475-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10844-017-0475-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10844-017-0475-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T19:27:15Z","timestamp":1750793235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10844-017-0475-2"}},"subtitle":["Formalization of the imperative core and translation into PRISM"],"short-title":[],"issued":{"date-parts":[[2017,8,1]]},"references-count":13,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,6]]}},"alternative-id":["475"],"URL":"https:\/\/doi.org\/10.1007\/s10844-017-0475-2","relation":{},"ISSN":["0925-9902","1573-7675"],"issn-type":[{"type":"print","value":"0925-9902"},{"type":"electronic","value":"1573-7675"}],"subject":[],"published":{"date-parts":[[2017,8,1]]},"assertion":[{"value":"2 January 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 May 2017","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 July 2017","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 August 2017","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}