{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:25:23Z","timestamp":1770283523791,"version":"3.49.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030029272","type":"print"},{"value":"9783030029289","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02928-9_4","type":"book-chapter","created":{"date-parts":[[2018,11,12]],"date-time":"2018-11-12T08:01:38Z","timestamp":1542009698000},"page":"115-142","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Modeling Concurrency in Dafny"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-8039","authenticated-orcid":false,"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,11,13]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"4_CR2","unstructured":"Abrial, J.-R.: Mini-course around Event-B and Rodin, June 2011. \nhttps:\/\/www.microsoft.com\/en-us\/research\/video\/mini-course-around-event-b-and-rodin\/"},{"issue":"6","key":"4_CR3","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Softw. Tools Technol. Transf."},{"key":"4_CR4","unstructured":"Back, R.-J., Sere, K.: Action systems with synchronous communication. In: Olderog, E.-R. (ed.) Proceedings of the IFIP TC2\/WG2.1\/WG2.2\/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET 1994). IFIP Transactions, vol. A-56, pp. 107\u2013126. North-Holland, June 1994"},{"key":"4_CR5","volume-title":"Parallel Program Design: A Foundation","author":"KM Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Boston (1988)"},{"key":"4_CR6","unstructured":"Dafny online (2017). \nhttp:\/\/rise4fun.com\/dafny"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings of the Symposium on Applied Mathematics, vol. 19, pp. 19\u201332. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"4_CR8","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D Gries","year":"1981","unstructured":"Gries, D.: The Science of Programming. MCS. Springer-Verlag, New York (1981). \nhttps:\/\/doi.org\/10.1007\/978-1-4612-5983-1"},{"issue":"3","key":"4_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2187671.2187678","volume":"44","author":"John Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1\u201316:58 (2012)","journal-title":"ACM Computing Surveys"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., et al.: IronFleet: proving practical distributed systems correct. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, pp. 1\u201317. ACM, October 2015","DOI":"10.1145\/2815400.2815428"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-642-35746-6_6","volume-title":"Tools for Practical Software Verification","author":"L Herbert","year":"2012","unstructured":"Herbert, L., Leino, K.R.M., Quaresma, J.: Using Dafny, an automatic program verifier. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 156\u2013181. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-35746-6_6"},{"issue":"10","key":"4_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013583 (1969)","journal-title":"Commun. ACM"},{"key":"4_CR13","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"4_CR14","unstructured":"Koenig, J., Leino, K.R.M.: Getting started with Dafny: a guide. In: Nipkow, T., Grumberg, O., Hauptmann, B. (eds.) Software Safety and Security: Tools for Analysis and Verification. NATO Science for Peace and Security Series D: Information and Communication Security, vol. 33, pp. 152\u2013181. IOS Press (2012). Summer School Marktoberdorf 2011 lecture notes"},{"key":"4_CR15","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","year":"2002","unstructured":"Lamport, L. (ed.): Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional, Boston (2002)"},{"key":"4_CR16","unstructured":"Lamport, L.: The TLA+ video course, March 2017. \nhttp:\/\/lamport.azurewebsites.net\/video\/videos.html"},{"key":"4_CR17","unstructured":"Leino, K.R.M.: Specification and verification of object-oriented software. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security. NATO Science for Peace and Security Series D: Information and Communication Security, vol. 22, pp. 231\u2013266. IOS Press (2009). Summer School Marktoberdorf 2008 lecture notes"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Developing verified programs with Dafny. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) 35th International Conference on Software Engineering, ICSE 2013, pp. 1488\u20131490. IEEE Computer Society (2013)","DOI":"10.1109\/ICSE.2013.6606754"},{"issue":"6","key":"4_CR20","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1109\/MS.2017.4121212","volume":"34","author":"KRM Leino","year":"2017","unstructured":"Leino, K.R.M.: Accessible software verification with Dafny. IEEE Software 34(6), 94\u201397 (2017)","journal-title":"IEEE Software"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02928-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,11,12]],"date-time":"2018-11-12T08:02:33Z","timestamp":1542009753000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02928-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030029272","9783030029289"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02928-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chongqing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.swu-rise.net.cn\/SETSS2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}