{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:45Z","timestamp":1750220685409,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319576657"},{"type":"electronic","value":"9783319576664"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57666-4_7","type":"book-chapter","created":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T12:18:42Z","timestamp":1491999522000},"page":"92-110","source":"Crossref","is-referenced-by-count":2,"title":["Constrained Synthesis from Component Libraries"],"prefix":"10.1007","author":[{"given":"Antonio","family":"Iannopollo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,13]]},"reference":[{"unstructured":"Semiconductor IP Market by Form Factor (ICs IP, SOCs IP), Design Architecture (IP cores (Hard IP, Soft IP), Standard IP, Custom IP, Processor Design), Processor Type (Microprocessor, DSP), Verification IP - Global forecast to 2022. marketsandmarkets.com (2016)","key":"7_CR1"},{"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, ESEC\/FSE-9, pp. 109\u2013120. ACM, New York (2001)","key":"7_CR2","DOI":"10.1145\/503209.503226"},{"doi-asserted-by":"crossref","unstructured":"Alur, R., Moarref, S., Topcu, U.: Compositional synthesis with parametric reactive controllers. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 215\u2013224. ACM, New York (2016)","key":"7_CR3","DOI":"10.1145\/2883817.2883842"},{"key":"7_CR4","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: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 200\u2013225. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-92188-2_9"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_22"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). doi: 10.1007\/10722167_15"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 62\u201373. ACM, New York (2011)","key":"7_CR8","DOI":"10.1145\/1993498.1993506"},{"doi-asserted-by":"crossref","unstructured":"Iannopollo, A., Nuzzo, P., Tripakis, S., Sangiovanni-Vincentelli, A.: Library-based scalable refinement checking for contract-based design. In: Design, Automation and Test in Europe Conference and Exhibition (DATE), pp. 1\u20136, March 2014","key":"7_CR9","DOI":"10.7873\/DATE.2014.167"},{"unstructured":"Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. CoRR abs\/1505.03953 (2015)","key":"7_CR10"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-642-00596-1_28","volume-title":"Foundations of Software Science and Computational Structures","author":"Y Lustig","year":"2009","unstructured":"Lustig, Y., Vardi, M.Y.: Synthesis from component libraries. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 395\u2013409. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-00596-1_28"},{"key":"7_CR12","doi-asserted-by":"crossref","DOI":"10.1002\/9780470770931","volume-title":"Aircraft Systems: Mechanical, Electrical and Avionics Subsystems Integration","author":"I Moir","year":"2008","unstructured":"Moir, I., Seabridge, A.: Aircraft Systems: Mechanical, Electrical and Avionics Subsystems Integration, 3rd edn. Wiley, Chichester (2008)","edition":"3"},{"doi-asserted-by":"crossref","unstructured":"Nuzzo, P., Finn, J., Iannopollo, A., Sangiovanni-Vincentelli, A.: Contract-based design of control protocols for safety-critical cyber-physical systems. In: Design, Automation and Test in Europe Conference and Exhibition (DATE), pp. 1\u20134, March 2014","key":"7_CR13","DOI":"10.7873\/DATE.2014.072"},{"doi-asserted-by":"crossref","unstructured":"Nuzzo, P., Iannopollo, A., Tripakis, S., Sangiovanni-Vincentelli, A.: Are interface theories equivalent to contract theories? In: 2014 Twelfth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 104\u2013113, October 2014","key":"7_CR14","DOI":"10.1109\/MEMCOD.2014.6961848"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: 31st Annual Symposium on Foundations of Computer Science, Proceedings, vol. 2, pp. 746\u2013757, October 1990","key":"7_CR15","DOI":"10.1109\/FSCS.1990.89597"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, pp. 46\u201357. IEEE Computer Society, Washington, DC (1977)","key":"7_CR16","DOI":"10.1109\/SFCS.1977.32"},{"issue":"3","key":"7_CR17","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1109\/JPROC.2006.890107","volume":"95","author":"A Sangiovanni-Vincentelli","year":"2007","unstructured":"Sangiovanni-Vincentelli, A.: Quo vadis, SLD? Reasoning about the trends and challenges of system level design. Proc. IEEE 95(3), 467\u2013506 (2007)","journal-title":"Proc. IEEE"},{"issue":"3","key":"7_CR18","doi-asserted-by":"crossref","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)","journal-title":"Eur. J. Control"},{"issue":"11","key":"7_CR19","doi-asserted-by":"crossref","first-page":"2036","DOI":"10.1109\/JPROC.2015.2471838","volume":"103","author":"SA Seshia","year":"2015","unstructured":"Seshia, S.A.: Combining induction, deduction, and structure for verification and synthesis. Proc. IEEE 103(11), 2036\u20132051 (2015)","journal-title":"Proc. IEEE"},{"key":"7_CR20","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1192.001.0001","volume-title":"Algorithmic Program DeBugging","author":"EY Shapiro","year":"1983","unstructured":"Shapiro, E.Y.: Algorithmic Program DeBugging. MIT Press, Cambridge (1983)"},{"issue":"3","key":"7_CR21","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"issue":"5","key":"7_CR22","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1145\/1168917.1168907","volume":"40","author":"A Solar-Lezama","year":"2006","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. SIGOPS Oper. Syst. Rev. 40(5), 404\u2013415 (2006)","journal-title":"SIGOPS Oper. Syst. Rev."},{"doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Topcu, U., Ozay, N., Xu, H., Murray, R.M.: Tulip: a software toolbox for receding horizon temporal logic planning. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, HSCC 2011, pp. 313\u2013314. ACM, New York (2011)","key":"7_CR23","DOI":"10.1145\/1967701.1967747"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57666-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:04:36Z","timestamp":1750197876000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57666-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319576657","9783319576664"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57666-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}