{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:00:38Z","timestamp":1743051638991,"version":"3.40.3"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319459424"},{"type":"electronic","value":"9783319459431"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","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":[[2016]]},"DOI":"10.1007\/978-3-319-45943-1_14","type":"book-chapter","created":{"date-parts":[[2016,9,12]],"date-time":"2016-09-12T13:31:17Z","timestamp":1473687077000},"page":"205-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System"],"prefix":"10.1007","author":[{"given":"Philip","family":"Johnson-Freyd","sequence":"first","affiliation":[]},{"given":"Geoffrey C.","family":"Hulette","sequence":"additional","affiliation":[]},{"given":"Zena M.","family":"Ariola","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,13]]},"reference":[{"issue":"2","key":"14_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theoret. Comput. Sci. 82(2), 253\u2013284 (1991)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"14_CR2","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3), 507\u2013535 (1995)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Abadi, M., Merz, S.: On TLA as a logic. In: Proceedings of the NATO Advanced Study Institute on Deductive Program Design, pp. 235\u2013271 (1996)","DOI":"10.1007\/978-3-642-61455-2_14"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14808-8_3","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"K Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA\n                      \n                        \n                      \n                      $$^ \\text{+ } $$\n                     proof system: building a heterogeneous verification platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 44\u201344. Springer, Heidelberg (2010)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BFb0055631","volume-title":"CONCUR \u201998 Concurrency Theory","author":"E Cohen","year":"1998","unstructured":"Cohen, E., Lamport, L.: Reduction in TLA. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 317\u2013331. Springer, Heidelberg (1998)"},{"key":"14_CR6","unstructured":"The Coq Development Team: The Coq proof assistant reference manual. LogiCal Project, Version 8.0 (2004)"},{"issue":"3","key":"14_CR7","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR8","unstructured":"Lamport, L.: Refinement in state-based formalisms. Technical report, DEC Systems Research Center (1996)"},{"key":"14_CR9","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co. Inc., Boston (2002)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Ricketts, D., Malecha, G., Alvarez, M.M., Gowda, V., Lerner, S. Towards verification of hybrid systems in a foundational proof assistant. In: MEMOCODE 2015, pp. 248\u2013257. IEEE (2015)","DOI":"10.1109\/MEMCOD.2015.7340492"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-40447-4_2","volume-title":"Trends in Functional Programming","author":"J Svenningsson","year":"2013","unstructured":"Svenningsson, J., Axelsson, E.: Combining deep and shallow embedding for EDSL. In: Loidl, H.-W., Pe\u00f1a, R. (eds.) TFP 2012. LNCS, vol. 7829, pp. 21\u201336. Springer, Heidelberg (2013)"},{"key":"14_CR12","first-page":"8","volume":"2014","author":"H Wan","year":"2014","unstructured":"Wan, H., He, A., You, Z., Zhao, X.: Formal proof of a machine closed theorem in Coq. J. Appl. Math. 2014, 8 (2014). Article ID 892832, Hindawi Publishing Corporation, Cairo","journal-title":"J. Appl. Math."},{"key":"14_CR13","unstructured":"Wenzel, M.: The Isabelle\/Isar Reference Manual (2012)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA\n                      \n                        \n                      \n                      $$^{+}$$\n                     specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Critical Systems: Formal Methods and Automated Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-45943-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:09:06Z","timestamp":1558314546000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-45943-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319459424","9783319459431"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-45943-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 September 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pisa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 September 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 September 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}