{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T03:26:07Z","timestamp":1743132367751,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030853143"},{"type":"electronic","value":"9783030853150"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-85315-0_9","type":"book-chapter","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T12:05:42Z","timestamp":1629374742000},"page":"134-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Mechanically Verified Theory of Contracts"],"prefix":"10.1007","author":[{"given":"St\u00e9phane","family":"Kastenbaum","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beno\u00eet","family":"Boyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,20]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M Abadi","year":"1993","unstructured":"Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Programm. Lang. Syst. 15(1), 73\u2013132 (1993). https:\/\/doi.org\/10.1145\/151646.151649","journal-title":"ACM Trans. Programm. Lang. Syst."},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Ar\u00e9chiga, N.: Specifying safety of autonomous vehicles in signal temporal logic. In: 2019 IEEE Intelligent Vehicles Symposium (IV), pp. 58\u201363 (2019). https:\/\/doi.org\/10.1109\/IVS.2019.8813875","DOI":"10.1109\/IVS.2019.8813875"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-92188-2_9","volume-title":"Formal Methods for Components and Objects","author":"A Benveniste","year":"2008","unstructured":"Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 200\u2013225. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-92188-2_9"},{"key":"9_CR4","unstructured":"Benveniste, A., et al.: Contracts for systems design: theory. Report, INRIA, July 2015"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/BFb0020972","volume-title":"Hybrid Systems III","author":"Z Chaochen","year":"1996","unstructured":"Chaochen, Z., Ji, W., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 511\u2013530. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020972"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-57318-6_23","volume-title":"Hybrid Systems","author":"Z Chaochen","year":"1993","unstructured":"Chaochen, Z., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 36\u201359. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_23"},{"key":"9_CR7","series-title":"NASA Monographs in Systems and Software Engineering","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-319-48628-4_3","volume-title":"Provably Correct Systems","author":"M Chen","year":"2017","unstructured":"Chen, M., et al.: MARS: a toolchain for modelling, analysis and verification of hybrid systems. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE, pp. 39\u201358. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-48628-4_3"},{"key":"9_CR8","volume-title":"Mastering Simulink","author":"JB Dabney","year":"2003","unstructured":"Dabney, J.B., Harman, T.L.: Mastering Simulink. Pearson, Upper Saddle River (2003)"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.tcs.2019.09.017","volume":"802","author":"S Foster","year":"2020","unstructured":"Foster, S., Cavalcanti, A., Canham, S., Woodcock, J., Zeyda, F.: Unifying theories of reactive design contracts. Theor. Comput. Sci. 802, 105\u2013140 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2019.09.017","journal-title":"Theor. Comput. Sci."},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-030-00244-2_2","volume-title":"Formal Methods for Industrial Critical Systems","author":"S Graf","year":"2018","unstructured":"Graf, S., Quinton, S., Girault, A., G\u00f6ssler, G.: Building correct cyber-physical systems: why we need a multiview contract theory. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 19\u201331. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00244-2_2"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-030-02450-5_6","volume-title":"Formal Methods and Software Engineering","author":"T Liebrenz","year":"2018","unstructured":"Liebrenz, T., Herber, P., Glesner, S.: Deductive verification of hybrid control systems modeled in simulink with KeYmaera X. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 89\u2013105. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02450-5_6"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-030-30942-8_22","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"S Lunel","year":"2019","unstructured":"Lunel, S., Mitsch, S., Boyer, B., Talpin, J.-P.: Parallel composition and modular verification of computer controlled systems in differential dynamic logic. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 354\u2013370. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_22"},{"issue":"10","key":"9_CR14","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u2018design by contract\u2019. Computer 25(10), 40\u201351 (1992). https:\/\/doi.org\/10.1109\/2.161279","journal-title":"Computer"},{"issue":"6","key":"9_CR15","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1007\/s10009-018-0502-9","volume":"20","author":"A M\u00fcller","year":"2018","unstructured":"M\u00fcller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: Tactical contract composition for hybrid system component verification. Int. J. Softw. Tools Technol. Transf. 20(6), 615\u2013643 (2018). https:\/\/doi.org\/10.1007\/s10009-018-0502-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"9_CR17","unstructured":"Nuzzo, P.: Compositional design of cyber-physical systems using contracts. Ph.D. thesis, UC Berkeley (2015)"},{"issue":"2","key":"9_CR18","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143\u2013189 (2008). https:\/\/doi.org\/10.1007\/s10817-008-9103-8","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9_CR19","doi-asserted-by":"publisher","first-page":"217","DOI":"10.3166\/ejc.18.217-238","volume":"18","author":"A Sangiovanni-Vincentelli","year":"2012","unstructured":"Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems*. Eur. J. Control 18(3), 217\u2013238 (2012). https:\/\/doi.org\/10.3166\/ejc.18.217-238","journal-title":"Eur. J. Control"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Team, T.C.D.: The Coq proof assistant, version 8.7.2. Zenodo, February 2018. https:\/\/doi.org\/10.5281\/zenodo.1174360","DOI":"10.5281\/zenodo.1174360"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-29952-0_13","volume-title":"Theory and Applications of Models of Computation","author":"S Wang","year":"2012","unstructured":"Wang, S., Zhan, N., Guelev, D.: An assume\/guarantee based compositional calculus for hybrid CSP. In: Agrawal, M., Cooper, S.B., Li, A. (eds.) TAMC 2012. LNCS, vol. 7287, pp. 72\u201383. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29952-0_13"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-25423-4_25","volume-title":"Formal Methods and Software Engineering","author":"S Wang","year":"2015","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382\u2013399. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_25"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-85315-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,27]],"date-time":"2021-08-27T00:02:36Z","timestamp":1630022556000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-85315-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030853143","9783030853150"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-85315-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2021.github.io\/","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":"55","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":"20","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":"0","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":"36% - 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":"3","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":"3","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}