{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:24:11Z","timestamp":1759332251518,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_23","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"477-493","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["From Interface Automata to\u00a0Hypercontracts"],"prefix":"10.1007","author":[{"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":[[2022,12,29]]},"reference":[{"issue":"1","key":"23_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. Program. Lang. Syst. 15(1), 73\u2013132 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 109\u2013120 ESEC\/FSE-9, Association for Computing Machinery, New York, NY, USA (2001)","DOI":"10.1145\/503209.503226"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45828-X_9","volume-title":"Embedded Software","author":"L de Alfaro","year":"2002","unstructured":"de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Timed interfaces. In: Sangiovanni-Vincentelli, A., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 108\u2013122. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45828-X_9"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR\u201998 Concurrency Theory","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163\u2013178. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055622"},{"key":"23_CR5","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Ferr\u00e8re, T., Henzinger, T.A., Nickovic, D., Da Costa, A.O.: Information-flow interfaces. In: Johnsen, E.B., Wimmer, M. (eds.) Fundamental Approaches to Software Engineering. FASE 2022. LNCS, vol. 13241, pp. 3\u201322. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7","DOI":"10.1007\/978-3-030-99429-7"},{"key":"23_CR6","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":"23_CR7","doi-asserted-by":"crossref","unstructured":"Benveniste, A., et al.: Contracts for system design. Foundations and Trends\u00ae in Electronic Design Automation, vol. 12(2\u20133), pp. 124\u2013400 (2018)","DOI":"10.1561\/1000000053"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","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., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource Interfaces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 117\u2013133. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45212-6_9"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"issue":"6","key":"23_CR10","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Damm, W.: Controlling speculative design processes using rich component models. In: Fifth International Conference on Application of Concurrency to System Design (ACSD2005), pp. 118\u2013119 (2005)","DOI":"10.1109\/ACSD.2005.35"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I\/O automata: a complete specification theory for real-time systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 91\u2013100. HSCC 2010, Association for Computing Machinery, New York, NY, USA (2010)","DOI":"10.1145\/1755952.1755967"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965)","DOI":"10.1145\/365559.365617"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Doyen, L., Henzinger, T.A., Jobstmann, B., Petrov, T.: Interface theories with component reuse. In: Proceedings of the 8th ACM International Conference on Embedded Software, pp. 79\u201388 EMSOFT 2008, Association for Computing Machinery, New York, NY, USA (2008)","DOI":"10.1145\/1450058.1450070"},{"key":"23_CR15","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Proceed. Symp. Appl. Math. 19, 19\u201332 (1967)","journal-title":"Proceed. Symp. Appl. Math."},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy. Oakland, CA, USA, April 26\u201328, 1982, pp. 11\u201320 IEEE Computer Society, Oakland, CA, USA (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"23_CR17","doi-asserted-by":"publisher","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, vol. 13, pp. 477\u2013498. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_17","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. SIGSOFT Softw. Eng. Notes 30(5), 31\u201340 (2005)","DOI":"10.1145\/1095430.1081713"},{"issue":"10","key":"23_CR19","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\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"23_CR20","unstructured":"Incer, I.: The algebra of contracts, Ph. D. thesis, EECS Department, University of California, Berkeley (2022)"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Incer, I., Benveniste, A., Sangiovanni-Vincentelli, A., Seshia, S.A.: Hypercontracts. arXiv preprint arXiv:2106.02449 (2021)","DOI":"10.1007\/978-3-031-06773-0_36"},{"key":"23_CR22","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, S.A.: Hypercontracts. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods, pp. 674\u2013692. Springer International Publishing, Cham (2022)"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Lamport, L.: The computer science of concurrency: the early years. Commun. ACM 58(6), 71\u201376 (2015)","DOI":"10.1145\/2771951"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-71316-6_6","volume-title":"Programming Languages and Systems","author":"KG Larsen","year":"2007","unstructured":"Larsen, K.G., Nyman, U., W\u0105sowski, A.: Modal I\/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64\u201379. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_6"},{"key":"23_CR25","first-page":"219","volume":"2","author":"NA Lynch","year":"1989","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI Quarterly 2, 219\u2013246 (1989)","journal-title":"CWI Quarterly"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","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.: Verifying bounded subset-closed hyperproperties. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 263\u2013283. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_17"},{"key":"23_CR27","unstructured":"Negulescu, R.: Process spacess. Tech. Rep. CS-95-48, University of Waterloo (1995)"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Parnas, D.L.: A technique for software module specification with examples. Commun. ACM 15(5), 330\u2013336 (1972)","DOI":"10.1145\/355602.361309"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Passerone, R., Incer, I., Sangiovanni-Vincentelli, A.L.: Coherent extension, composition, and merging operators in contract models for system design. ACM Trans. Embed. Comput. Syst. 18(5s), 1\u201323 (2019)","DOI":"10.1145\/3358216"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977)(FOCS), pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"23_CR31","unstructured":"Rabe, M.N.: A temporal logic approach to information-flow control, Ph. D. thesis, Universit\u00e4t des Saarlandes (2016)"},{"key":"23_CR32","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.entcs.2008.06.023","volume":"215","author":"J Raclet","year":"2008","unstructured":"Raclet, J.: Residual for component specifications. Electr. Notes Theor. Comput. Sci. 215, 93\u2013110 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"23_CR33","first-page":"119","volume":"108","author":"JB Raclet","year":"2011","unstructured":"Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fund. Inform. 108(1\u20132), 119\u2013149 (2011)","journal-title":"Fund. Inform."},{"key":"23_CR34","doi-asserted-by":"crossref","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)","DOI":"10.3166\/ejc.18.217-238"},{"key":"23_CR35","doi-asserted-by":"crossref","unstructured":"Sifakis, J.: Rigorous system design. Foundations and Trends\u00ae in Electronic Design Automation, vol. 6, no. 4, pp. 293\u2013362 (2013)","DOI":"10.1561\/1000000034"},{"key":"23_CR36","unstructured":"Turing, A.M.: On checking a large routine. In: Report of a Conference on High-Speed Automatic Calculating Machines, pp. 67\u201369. University Mathematical Laboratory, Cambridge (1949)"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T02:55:24Z","timestamp":1728615324000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}