{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:12:43Z","timestamp":1763968363408,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030309411"},{"type":"electronic","value":"9783030309428"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-30942-8_11","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"161-178","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems"],"prefix":"10.1007","author":[{"given":"Yongwang","family":"Zhao","sequence":"first","affiliation":[]},{"given":"David","family":"San\u00e1n","sequence":"additional","affiliation":[]},{"given":"Fuyuan","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"11_CR1","unstructured":"The Zephyr Project. \nhttps:\/\/www.zephyrproject.org\/\n\n. Accessed December 2018"},{"issue":"1\u20132","key":"11_CR2","first-page":"1","volume":"77","author":"JR Abrial","year":"2007","unstructured":"Abrial, J.R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to event-B. Fundamenta Informaticae 77(1\u20132), 1\u201328 (2007)","journal-title":"Fundamenta Informaticae"},{"key":"11_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814105","volume-title":"Reactive Systems - Modeling, Specification and Verification","author":"L Aceto","year":"2007","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K., Srba, J.: Reactive Systems - Modeling, Specification and Verification. Cambridge University Press, Cambridge (2007)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Andronick, J., Lewis, C., Morgan, C.: Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system. In: Proceedings Workshop on Models for Formal Analysis of Real Systems MARS, pp. 10\u201324 (2015)","DOI":"10.4204\/EPTCS.196.2"},{"issue":"3","key":"11_CR5","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/BF01214918","volume":"8","author":"RJ Back","year":"1996","unstructured":"Back, R.J., Sere, K.: Superposition Refinement of Reactive Systems. Formal Aspects Comput. 8(3), 324\u2013346 (1996)","journal-title":"Formal Aspects Comput."},{"key":"11_CR6","first-page":"17","volume":"12","author":"RJ Back","year":"1991","unstructured":"Back, R.J., Sere, K.: Stepwise refinement of action systems. Struct. Program. 12, 17\u201330 (1991)","journal-title":"Struct. Program."},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Chen, H., Wu, X., Shao, Z., Lockerman, J., Gu, R.: Toward compositional verification of interruptible OS kernels and device drivers. In: 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 431\u2013447. ACM (2016)","DOI":"10.1145\/2980983.2908101"},{"issue":"3","key":"11_CR8","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s001650050011","volume":"10","author":"J Dingel","year":"1998","unstructured":"Dingel, J., Garlan, D., Jha, S., Notkin, D.: Towards a formal treatment of implicit invocation using rely\/guarantee reasoning. Formal Aspects Comput. 10(3), 193\u2013213 (1998)","journal-title":"Formal Aspects Comput."},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-36578-8_6","volume-title":"Fundamental Approaches to Software Engineering","author":"P Fenkam","year":"2003","unstructured":"Fenkam, P., Gall, H., Jazayeri, M.: Composing specifications of event based applications. In: Pezz\u00e8, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 67\u201386. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-36578-8_6"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"636","DOI":"10.1007\/978-3-540-45236-2_35","volume-title":"FME 2003: Formal Methods","author":"P Fenkam","year":"2003","unstructured":"Fenkam, P., Gall, H., Jazayeri, M.: Constructing deadlock free event-based applications: a rely\/guarantee approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 636\u2013657. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-45236-2_35"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Garlan, D., Jha, S., Notkin, D., Dingel, J.: Reasoning about implicit invocation. In: Proceedings of the 6th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pp. 209\u2013221. ACM, New York (1998)","DOI":"10.1145\/291252.288312"},{"key":"11_CR12","series-title":"NATO ASI Series (Series F: Computer and Systems Sciences)","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-82453-1_17","volume-title":"Logics and Models of Concurrent Systems","author":"D Harel","year":"1985","unstructured":"Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 13, pp. 477\u2013498. Springer, Heidelberg (1985). \nhttps:\/\/doi.org\/10.1007\/978-3-642-82453-1_17"},{"issue":"6","key":"11_CR13","doi-asserted-by":"publisher","first-page":"1057","DOI":"10.1007\/s00165-016-0384-0","volume":"28","author":"IJ Hayes","year":"2016","unstructured":"Hayes, I.J.: Generalised rely-guarantee concurrency: an algebraic foundation. Formal Aspects Comput. 28(6), 1057\u20131078 (2016)","journal-title":"Formal Aspects Comput."},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-319-48989-6_22","volume-title":"FM 2016: Formal Methods","author":"IJ Hayes","year":"2016","unstructured":"Hayes, I.J., Colvin, R.J., Meinicke, L.A., Winter, K., Velykis, A.: An algebra of synchronous atomic steps. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 352\u2013369. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-48989-6_22"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-642-11811-1_24","volume-title":"Abstract State Machines, Alloy, B and Z","author":"TS Hoang","year":"2010","unstructured":"Hoang, T.S., Abrial, J.-R.: Event-B decomposition for parallel programs. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 319\u2013333. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-11811-1_24"},{"issue":"4","key":"11_CR16","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009, Big Sky, Montana, USA, pp. 207\u2013220. ACM Press (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X., Fu, M.: A rely-guarantee-based simulation for verifying concurrent program transformations. In: 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 455\u2013468. ACM Press (2012)","DOI":"10.1145\/2103621.2103711"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: 24th Computer Security Foundations Symposium (CSF), pp. 218\u2013232. IEEE Press (2011)","DOI":"10.1109\/CSF.2011.22"},{"key":"11_CR20","unstructured":"Moreira, N., Pereira, D., de Sousa, S.M.: On the mechanisation of rely-guarantee in Coq. Universidade do Porto, Technical report (2013)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-35308-6_12","volume-title":"Certified Programs and Proofs","author":"T Murray","year":"2012","unstructured":"Murray, T., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 126\u2013142. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-35308-6_12"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Murray, T., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: 29th IEEE Computer Security Foundations Symposium (CSF). IEEE Press (2016)","DOI":"10.1109\/CSF.2016.36"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-36575-3_24","volume-title":"Programming Languages and Systems","author":"LP Nieto","year":"2003","unstructured":"Nieto, L.P.: The rely-guarantee method in Isabelle\/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 348\u2013362. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-36575-3_24"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-662-54577-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D San\u00e1n","year":"2017","unstructured":"San\u00e1n, D., Zhao, Y., Hou, Z., Zhang, F., Tiu, A., Liu, Y.: CSimpl: a rely-guarantee-based framework for verifying concurrent programs. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 481\u2013498. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54577-5_28"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. Ph.D. thesis, Technical University Munich (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-19797-5_2","volume-title":"Mathematics of Program Construction","author":"S van Staden","year":"2015","unstructured":"van Staden, S.: On rely-guarantee reasoning. In: Hinze, R., Voigtl\u00e4nder, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 30\u201349. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19797-5_2"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-319-41540-6_4","volume-title":"Computer Aided Verification","author":"F Xu","year":"2016","unstructured":"Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 59\u201379. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41540-6_4"},{"issue":"2","key":"11_CR28","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput. 9(2), 149\u2013174 (1997)","journal-title":"Formal Aspects Comput."},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-030-25543-5_29","volume-title":"Computer Aided Verification","author":"Y Zhao","year":"2019","unstructured":"Zhao, Y., San\u00e1n, D.: Rely-guarantee reasoning about concurrent memory management in Zephyr RTOS. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 515\u2013533. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-25543-5_29"}],"container-title":["Lecture Notes in Computer Science","Formal Methods \u2013 The Next 30 Years"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30942-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,5]],"date-time":"2020-05-05T06:07:44Z","timestamp":1588658864000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30942-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309411","9783030309428"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30942-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","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":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"129","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}