{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,6]],"date-time":"2026-01-06T18:51:55Z","timestamp":1767725515946,"version":"build-2238731810"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T00:00:00Z","timestamp":1749513600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T00:00:00Z","timestamp":1749513600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100006502","name":"Defense Sciences Office, DARPA","doi-asserted-by":"publisher","award":["FA8750-20-C-0156"],"award-info":[{"award-number":["FA8750-20-C-0156"]}],"id":[{"id":"10.13039\/100006502","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1739816"],"award-info":[{"award-number":["1739816"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100015488","name":"Office for Science and Technology of the Embassy of France in the United States","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100015488","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000850","name":"American Society for Engineering Education","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000850","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Contract theories have been proposed to formally support distributed and decentralized system design while ensuring safe system integration. This paper introduces\n                    <jats:italic>hypercontracts<\/jats:italic>\n                    , a compositional assume-guarantee formalism that supports the expression and manipulation of hyperproperties of arbitrary structure. Hyperproperties can express characteristics such as mean response times, security attributes, and robustness that lie outside the expressivity of trace properties and contracts. By considering hyperproperties with interval and downward closed structure, we obtain specializations of the theory of hypercontracts to\n                    <jats:italic>interval<\/jats:italic>\n                    and\n                    <jats:italic>conic<\/jats:italic>\n                    hypercontracts. These specializations are more general than assume-guarantee contracts but come with finite descriptions, while enabling new applications of contracts in security and autonomous cyber-physical system design.\n                  <\/jats:p>","DOI":"10.1007\/s10703-025-00473-6","type":"journal-article","created":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T11:58:28Z","timestamp":1749556708000},"page":"455-497","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Hypercontracts"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7933-692X","authenticated-orcid":false,"given":"Inigo","family":"Incer","sequence":"first","affiliation":[]},{"given":"Albert","family":"Benveniste","sequence":"additional","affiliation":[]},{"given":"Alberto","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,6,10]]},"reference":[{"issue":"3","key":"473_CR1","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1109\/JPROC.2006.890107","volume":"95","author":"A Sangiovanni-Vincentelli","year":"2007","unstructured":"Sangiovanni-Vincentelli A (2007) Quo vadis, SLD? Reasoning about the trends and challenges of system level design. Proc IEEE 95(3):467\u2013506","journal-title":"Proc IEEE"},{"key":"473_CR2","doi-asserted-by":"crossref","unstructured":"Sifakis J (2014) Toward a system design science. In: From programs to systems. The systems perspective in computing: ETAPS workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings. Springer, pp. 225\u2013234","DOI":"10.1007\/978-3-642-54848-2_15"},{"key":"473_CR3","doi-asserted-by":"crossref","unstructured":"Alfaro L, Henzinger TA (2001) Interface automata. In: Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on foundations of software engineering. ESEC\/FSE-9. Association for Computing Machinery, New York, NY, USA, pp 109\u2013120","DOI":"10.1145\/503209.503226"},{"key":"473_CR4","first-page":"148","volume-title":"EMSOFT\u201901","author":"L Alfaro","year":"2001","unstructured":"Alfaro L, Henzinger TA (2001) Interface theories for component-based design. In: Henzinger TA, Kirsch CM (eds) EMSOFT\u201901. Springer, Berlin, pp 148\u2013165"},{"key":"473_CR5","doi-asserted-by":"crossref","unstructured":"Doyen L, Henzinger TA, Jobstmann B, Petrov T (2008) Interface theories with component reuse. In: Proceedings of the 8th ACM and IEEE international conference on embedded software, EMSOFT\u201908, Atlanta, GA, pp 79\u201388","DOI":"10.1145\/1450058.1450070"},{"key":"473_CR6","doi-asserted-by":"crossref","unstructured":"L\u00fcttgen G, Vogler W (2013) Modal interface automata. Logical Methods Computer Sci 9(3)","DOI":"10.2168\/LMCS-9(3:4)2013"},{"key":"473_CR7","doi-asserted-by":"crossref","unstructured":"Bujtor F, Vogler W (2014) Error-pruning in interface automata. In: 40th international conference on current trends in theory and practice of computer science. SOFSEM 2014. Nov\u00fd Smokovec, Slovakia, pp 162\u2013173","DOI":"10.1007\/978-3-319-04298-5_15"},{"key":"473_CR8","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/3-540-44618-4_16","volume-title":"CONCUR 2000 \u2013 Concurrency Theory","author":"R Negulescu","year":"2000","unstructured":"Negulescu R (2000) Process spaces. In: Palamidessi C (ed) CONCUR 2000 \u2013 Concurrency Theory. Springer, Berlin, pp 199\u2013213"},{"key":"473_CR9","doi-asserted-by":"crossref","unstructured":"Larsen KG, Nyman U, Wasowski A (2006) Interface input\/output automata. In: FM, pp 82\u201397","DOI":"10.1007\/11813040_7"},{"key":"473_CR10","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-540-74407-8_8","volume-title":"CONCUR 2007 - Concurrency Theory","author":"KG Larsen","year":"2007","unstructured":"Larsen KG, Nyman U, W\u0105sowski A (2007) On modal refinement and consistency. In: Caires L, Vasconcelos VT (eds) CONCUR 2007 - Concurrency Theory. Springer, Berlin, pp 105\u2013119"},{"key":"473_CR11","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-71316-6_6","volume-title":"Programming languages and systems, 16th European symposium on programming, ESOP\u201907","author":"KG Larsen","year":"2007","unstructured":"Larsen KG, Nyman U, W\u0105sowski A (2007) Modal I\/O automata for interface and product line theories. In: De Nicola R (ed) Programming languages and systems, 16th European symposium on programming, ESOP\u201907. Springer, Berlin, pp 64\u201379"},{"key":"473_CR12","doi-asserted-by":"crossref","unstructured":"Raclet J-B, Badouel E, Benveniste A, Caillaud B, Legay A, Passerone R (2009) Modal interfaces: Unifying interface automata and modal specifications. In: Proceedings of the seventh ACM international conference on embedded software. EMSOFT \u201909. Association for Computing Machinery, New York, NY, USA, pp 87\u201396","DOI":"10.1145\/1629335.1629348"},{"key":"473_CR13","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1016\/j.scico.2013.06.003","volume":"83","author":"SS Bauer","year":"2014","unstructured":"Bauer SS, Larsen KG, Legay A, Nyman U, Wasowski A (2014) A modal specification theory for components with data. Sci Comput Program 83:106\u2013128","journal-title":"Sci Comput Program"},{"key":"473_CR14","doi-asserted-by":"crossref","unstructured":"Benveniste A, Caillaud B, Ferrari A, Mangeruca L, Passerone R, Sofronis C (2008) Multiple viewpoint contract-based specification and design. In: Boer FS, Bonsangue MM, Graf S, Roever W-P (eds) Formal methods for components and objects: 6th international symposium, FMCO 2007, Amsterdam, The Netherlands, October 24\u201326, 2007, Revised Lectures. Springer, Berlin, pp 200\u2013225","DOI":"10.1007\/978-3-540-92188-2_9"},{"key":"473_CR15","unstructured":"Jones CB (1983) Specification and design of (parallel) programs. In: IFIP Congress, Paris, France, pp 321\u2013332"},{"key":"473_CR16","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-0-387-21798-7_1","volume-title":"Programming methodology","author":"CB Jones","year":"2003","unstructured":"Jones CB (2003) Wanted: a compositional approach to concurrency. In: McIver A, Morgan C (eds) Programming methodology. Springer, New York, pp 5\u201315"},{"issue":"4","key":"473_CR17","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1093\/logcom\/exm030","volume":"17","author":"JW Coleman","year":"2007","unstructured":"Coleman JW, Jones CB (2007) A structural proof of the soundness of rely\/guarantee rules. J Log Comput 17(4):807\u2013841","journal-title":"J Log Comput"},{"key":"473_CR18","doi-asserted-by":"crossref","unstructured":"Hayes IJ, Jones CB (2017) A guide to rely\/guarantee thinking. In: Bowen JP, Liu Z, Zhang Z (eds) Engineering trustworthy software systems - third international school, SETSS 2017, Chongqing, China, April 17\u201322, 2017, Tutorial Lectures. Springer, Cham, pp 1\u201338","DOI":"10.1007\/978-3-030-02928-9_1"},{"key":"473_CR19","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.-B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T.A., Larsen, K.G.: Contracts for system design. Foundations and Trendsr\u00ae in Electron Design Autom 12(2-3), 124\u2013400 (2018)","DOI":"10.1561\/1000000053"},{"key":"473_CR20","doi-asserted-by":"crossref","unstructured":"Goguen JA, Meseguer J (1982) Security policies and security models. In: 1982 IEEE symposium on security and privacy, Oakland, CA, USA, April 26\u201328, 1982. IEEE Computer Society, Oakland, CA, USA, pp 11\u201320","DOI":"10.1109\/SP.1982.10014"},{"key":"473_CR21","doi-asserted-by":"crossref","unstructured":"Seshia SA, Desai A, Dreossi T, Fremont D, Ghosh S, Kim E, Shivakumar S, Vazquez-Chanlatte M, Yue X (2018) Formal specification for deep neural networks. In: Proceedings of the international symposium on automated technology for verification and analysis (ATVA), pp 20\u201334","DOI":"10.1007\/978-3-030-01090-4_2"},{"issue":"6","key":"473_CR22","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson MR, Schneider FB (2010) Hyperproperties. J Comput Secur 18(6):1157\u20131210","journal-title":"J Comput Secur"},{"key":"473_CR23","unstructured":"Rabe MN (2016) A temporal logic approach to information-flow control. Ph.D. thesis, Universit\u00e4t des Saarlandes"},{"key":"473_CR24","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-319-99725-4_17","volume-title":"Static analysis","author":"I Mastroeni","year":"2018","unstructured":"Mastroeni I, Pasqua M (2018) Verifying bounded subset-closed hyperproperties. In: Podelski A (ed) Static analysis. Springer, Cham, pp 263\u2013283"},{"key":"473_CR25","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-28872-2_3","volume-title":"Fundamental approaches to software engineering","author":"SS Bauer","year":"2012","unstructured":"Bauer SS, David A, Hennicker R, Larsen KG, Legay A, Nyman U, W\u0105sowski A (2012) Moving from specifications to contracts in component-based design. In: Lara J, Zisman A (eds) Fundamental approaches to software engineering. Springer, Berlin, pp 43\u201358"},{"key":"473_CR26","unstructured":"Incer Romeo I (2022) The algebra of contracts. Ph.D. thesis, EECS Department, University of California, Berkeley"},{"key":"473_CR27","doi-asserted-by":"publisher","first-page":"674","DOI":"10.1007\/978-3-031-06773-0_36","volume-title":"NASA formal methods","author":"I Incer","year":"2022","unstructured":"Incer I, Benveniste A, Sangiovanni-Vincentelli A, Seshia SA (2022) Hypercontracts. In: Deshmukh JV, Havelund K, Perez I (eds) NASA formal methods. Springer, Cham, pp 674\u2013692"},{"key":"473_CR28","doi-asserted-by":"publisher","unstructured":"Incer I, Benveniste A, Sangiovanni-Vincentelli A, Seshia SA (2022) From interface automata to hypercontracts. In: Raskin, J.-F., Chatterjee, K., Doyen, L., Majumdar, R. (eds.) Principles of systems design: essays dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. Springer, Cham, pp 477\u2013493. https:\/\/doi.org\/10.1007\/978-3-031-22337-2_23","DOI":"10.1007\/978-3-031-22337-2_23"},{"key":"473_CR29","doi-asserted-by":"crossref","unstructured":"Incer I, Mangeruca L, Villa T, Sangiovanni-Vincentelli AL (2020) The quotient in preorder theories. In: Raskin J-F, Bresolin D (eds) Proceedings 11th international symposium on games, automata, logics, and formal verification, vol 326. Electronic Proceedings in Theoretical Computer Science. Open Publishing Association, Brussels, pp 216\u2013233","DOI":"10.4204\/EPTCS.326.14"},{"issue":"1","key":"473_CR30","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M Abadi","year":"1993","unstructured":"Abadi M, Lamport L (1993) Composing specifications. ACM Trans Program Lang Syst 15(1):73\u2013132","journal-title":"ACM Trans Program Lang Syst"},{"key":"473_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68759-9","volume-title":"The unknown component problem: theory and applications","author":"T Villa","year":"2012","unstructured":"Villa T, Yevtushenko N, Brayton R, Mishchenko A, Petrenko A, Sangiovanni-Vincentelli A (2012) The unknown component problem: theory and applications. Springer, New York"},{"key":"473_CR32","doi-asserted-by":"crossref","unstructured":"Passerone R, Incer I, Sangiovanni-Vincentelli AL (2019) Coherent extension, composition, and merging operators in contract models for system design. ACM Trans Embed Comput Syst 18(5s)","DOI":"10.1145\/3358216"},{"issue":"3","key":"473_CR33","doi-asserted-by":"publisher","first-page":"217","DOI":"10.3166\/ejc.18.217-238","volume":"18","author":"AL Sangiovanni-Vincentelli","year":"2012","unstructured":"Sangiovanni-Vincentelli AL, Damm W, Passerone R (2012) Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur J Control 18(3):217\u2013238","journal-title":"Eur J Control"},{"key":"473_CR34","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-030-01090-4_2","volume-title":"Automated technology for verification and analysis","author":"SA Seshia","year":"2018","unstructured":"Seshia SA, Desai A, Dreossi T, Fremont DJ, Ghosh S, Kim E, Shivakumar S, Vazquez-Chanlatte M, Yue X (2018) Formal specification for deep neural networks. In: Lahiri SK, Wang C (eds) Automated technology for verification and analysis. Springer, Cham, pp 20\u201334"},{"key":"473_CR35","doi-asserted-by":"crossref","unstructured":"Raclet J-B, Badouel E, Benveniste A, Caillaud B, Legay A, Passerone R (2009) Modal interfaces: Unifying interface automata and modal specifications. In: Proceedings of the seventh ACM international conference on embedded software. EMSOFT\u201909, pp. 87\u201396. Association for Computing Machinery, New York, NY, USA","DOI":"10.1145\/1629335.1629348"},{"key":"473_CR36","first-page":"219","volume":"2","author":"NA Lynch","year":"1989","unstructured":"Lynch NA, Tuttle MR (1989) An introduction to input\/output automata. CWI Q 2:219\u2013246","journal-title":"CWI Q"},{"key":"473_CR37","doi-asserted-by":"crossref","unstructured":"Incer Romeo I, Sangiovanni-Vincentelli A, Lin C-W, Kang E (2018) Quotient for assume-guarantee contracts. In: 2018 16th ACM\/IEEE international conference on formal methods and models for system design (MEMOCODE). IEEE, pp 1\u201311","DOI":"10.1109\/MEMCOD.2018.8556872"},{"key":"473_CR38","unstructured":"Incer I, Benveniste A, Sangiovanni-Vincentelli A (2023) Some algebraic aspects of assume-guarantee reasoning. https:\/\/arxiv.org\/abs\/2309.08875"},{"key":"473_CR39","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-031-75380-0_18","volume-title":"Leveraging applications of formal methods, verification and validation. Specification and verification","author":"I Incer","year":"2025","unstructured":"Incer I (2025) Composition and merging of assume-guarantee contracts are tensor products. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation. Specification and verification. Springer, Cham, pp 320\u2013329"},{"key":"473_CR40","first-page":"57","volume":"41","author":"I Incer","year":"2024","unstructured":"Incer I (2024) An adjunction between Boolean algebras and a subcategory of stone algebras. Theory Appl Categ 41:57\u201320412057","journal-title":"Theory Appl Categ"},{"key":"473_CR41","unstructured":"Phan-Minh T, Murray RM (2019) Contracts of reactivity. Technical report, California Institute of Technology"},{"key":"473_CR42","unstructured":"Phan-Minh T (2021) Contract-based design: theories and applications. Ph.D. thesis, California Institute of Technology"},{"key":"473_CR43","doi-asserted-by":"crossref","unstructured":"Saoud A, Girard A, Fribourg L (2018) On the composition of discrete and continuous-time assume-guarantee contracts for invariance. In: 16th European control conference (ECC), June 12\u201315, 2018. IEEE, Limassol, Cyprus, pp 435\u2013440","DOI":"10.23919\/ECC.2018.8550622"},{"key":"473_CR44","doi-asserted-by":"crossref","unstructured":"Saoud A, Girard A, Fribourg L (2021) Assume-guarantee contracts for continuous-time systems. Working paper or preprint","DOI":"10.1016\/j.automatica.2021.109910"},{"key":"473_CR45","doi-asserted-by":"crossref","unstructured":"Li J, Nuzzo P, Sangiovanni-Vincentelli A, Xi Y, Li D (2017) Stochastic contracts for cyber-physical system design under probabilistic requirements. In: Proceedings of the 15th ACM-IEEE international conference on formal methods and models for system design. MEMOCODE\u201917. Association for Computing Machinery, New York, NY, USA, pp 5\u201314","DOI":"10.1145\/3127041.3127045"},{"issue":"5","key":"473_CR46","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.ifacol.2021.08.469","volume":"54","author":"M Sharf","year":"2021","unstructured":"Sharf M, Besselink B, Molin A, Zhao Q, Henrik Johansson K (2021) Assume\/guarantee contracts for dynamical systems: theory and computational tools. IFAC-PapersOnLine 54(5):25\u201330. https:\/\/doi.org\/10.1016\/j.ifacol.2021.08.469","journal-title":"IFAC-PapersOnLine"},{"key":"473_CR47","doi-asserted-by":"publisher","unstructured":"Girard A, Iovine A, Benberkane S (2022) Invariant sets for assume-guarantee contracts. In: 61st conference on decision and control (CDC), pp. 2190\u20132195. IEEE, Canc\u00fan, Mexico. https:\/\/doi.org\/10.1109\/CDC51059.2022.9993344","DOI":"10.1109\/CDC51059.2022.9993344"},{"key":"473_CR48","doi-asserted-by":"crossref","unstructured":"Alaoui SB, Saoud A (2024) Contract-based design for hybrid dynamical systems and invariance properties. arXiv preprint arXiv:2405.07718","DOI":"10.1016\/j.ifacol.2024.07.446"},{"key":"473_CR49","doi-asserted-by":"publisher","first-page":"1211","DOI":"10.1109\/LCSYS.2024.3410150","volume":"8","author":"I Incer","year":"2024","unstructured":"Incer I, Csomay-Shanklin N, Ames AD, Murray RM (2024) Layered control systems operating on multiple clocks. IEEE Control Syst Lett 8:1211\u20131216. https:\/\/doi.org\/10.1109\/LCSYS.2024.3410150","journal-title":"IEEE Control Syst Lett"},{"key":"473_CR50","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-540-45212-6_9","volume-title":"Embedded software","author":"A Chakrabarti","year":"2003","unstructured":"Chakrabarti A, Alfaro L, Henzinger TA, Stoelinga M (2003) Resource interfaces. In: Alur R, Lee I (eds) Embedded software. Springer, Berlin, pp 117\u2013133"},{"key":"473_CR51","doi-asserted-by":"publisher","DOI":"10.1145\/1985342.1985345","author":"S Tripakis","year":"2011","unstructured":"Tripakis S, Lickly B, Henzinger TA, Lee EA (2011) A theory of synchronous relational interfaces. ACM Trans Program Lang Syst. https:\/\/doi.org\/10.1145\/1985342.1985345","journal-title":"ACM Trans Program Lang Syst"},{"key":"473_CR52","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45828-X_9","volume-title":"Embedded software","author":"L Alfaro","year":"2002","unstructured":"Alfaro L, Henzinger TA, Stoelinga M (2002) Timed interfaces. In: Sangiovanni-Vincentelli A, Sifakis J (eds) Embedded software. Springer, Berlin, pp 108\u2013122"},{"key":"473_CR53","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-99429-7_1","volume-title":"Fundamental approaches to software engineering","author":"E Bartocci","year":"2022","unstructured":"Bartocci E, Ferr\u00e8re T, Henzinger TA, Nickovic D, Costa AO (2022) Information-flow interfaces. In: Johnsen EB, Wimmer M (eds) Fundamental approaches to software engineering. Springer, Cham, pp 3\u201322"},{"key":"473_CR54","unstructured":"Benveniste A, Raclet J-B, Caillaud B, Nickovic D, Passerone R, Sangiovanni-Vincentelli A, Henzinger T, Larsen K (2011) Contracts for the design of embedded systems, part ii: theory (submitted for publication)"},{"key":"473_CR55","doi-asserted-by":"crossref","unstructured":"Bauer SS, David A, Hennicker R, Larsen KG, Legay A, Nyman U, W\u0105sowski A (2012) In: Lara J, Zisman A (eds) Moving from specifications to contracts in component-based design. Springer, Berlin, pp 43\u201358","DOI":"10.1007\/978-3-642-28872-2_3"},{"key":"473_CR56","doi-asserted-by":"crossref","unstructured":"Nyberg M, Westman J, Gurov D (2020) Formally proving compositionality in industrial systems with informal specifications. In: Leveraging applications of formal methods, verification and validation: applications: 9th international symposium on leveraging applications of formal methods, ISoLA 2020, Rhodes, Greece, October 20\u201330, 2020, Proceedings, Part III 9. Springer, pp 348\u2013365","DOI":"10.1007\/978-3-030-61467-6_22"},{"issue":"3","key":"473_CR57","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/s10703-019-00334-z","volume":"54","author":"B Finkbeiner","year":"2019","unstructured":"Finkbeiner B, Hahn C, Stenger M, Tentrup L (2019) Monitoring hyperproperties. Form Methods Syst Design 54(3):336\u2013363","journal-title":"Form Methods Syst Design"}],"updated-by":[{"DOI":"10.1007\/s10703-025-00485-2","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T00:00:00Z","timestamp":1754352000000}}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00473-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00473-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00473-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,30]],"date-time":"2025-09-30T15:26:43Z","timestamp":1759246003000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00473-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":57,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["473"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00473-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"12 January 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 February 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 June 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 August 2025","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The original online version of this article was revised. In this article in Figure 1 Panel (a) was erroneously published with inverted colors.","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 August 2025","order":7,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":8,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":9,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s10703-025-00485-2","URL":"https:\/\/doi.org\/10.1007\/s10703-025-00485-2","order":10,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}