{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T16:23:40Z","timestamp":1759335820093,"version":"3.37.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319961446"},{"type":"electronic","value":"9783319961453"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_16","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T18:25:55Z","timestamp":1532111155000},"page":"289-306","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Synthesizing Reactive Systems from Hyperproperties"],"prefix":"10.1007","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christopher","family":"Hahn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1003-3573","authenticated-orcid":false,"given":"Philip","family":"Lukert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marvin","family":"Stenger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6150-2982","authenticated-orcid":false,"given":"Leander","family":"Tentrup","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in HyperLTL. In: Proceedings of CSF, pp. 239\u2013252. IEEE Computer Society (2016)","DOI":"10.1109\/CSF.2016.24"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Brewer, E.A.: Towards robust distributed systems (abstract). In: Proceedings of ACM, p. 7. ACM (2000)","DOI":"10.1145\/343477.343502"},{"issue":"10","key":"16_CR3","doi-asserted-by":"crossref","first-page":"1030","DOI":"10.1145\/4372.4373","volume":"28","author":"D Chaum","year":"1985","unstructured":"Chaum, D.: Security without identification: transaction systems to make big brother obsolete. Commun. ACM 28(10), 1030\u20131044 (1985)","journal-title":"Commun. ACM"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"16_CR5","doi-asserted-by":"crossref","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":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-27940-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Dimitrova","year":"2012","unstructured":"Dimitrova, R., Finkbeiner, B., Kov\u00e1cs, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 169\u2013185. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-27940-9_12"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-662-54577-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354\u2013370. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54577-5_20"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-63390-9_17","volume-title":"Computer Aided Verification","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: an experimentation framework for bounded synthesis. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 325\u2013332. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63390-9_17"},{"key":"16_CR9","unstructured":"Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: Proceedings of CONCUR. LIPIcs, vol. 59, pp. 13:1\u201313:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-67531-2_12","volume-title":"Runtime Verification","author":"B Finkbeiner","year":"2017","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 190\u2013207. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-67531-2_12"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-27940-9_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Finkbeiner","year":"2012","unstructured":"Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 219\u2013234. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-27940-9_15"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-21690-4_3","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2015","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^*$$\u2217. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30\u201348. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_3"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Proceedings of LICS, pp. 321\u2013330. IEEE Computer Society (2005)","DOI":"10.1109\/LICS.2005.53"},{"issue":"5\u20136","key":"16_CR14","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5\u20136), 519\u2013539 (2013)","journal-title":"STTT"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-54862-8_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Finkbeiner","year":"2014","unstructured":"Finkbeiner, B., Tentrup, L.: Detecting unrealizable specifications of distributed systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 78\u201392. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54862-8_6"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Tentrup, L.: Detecting unrealizability of distributed fault-tolerant systems. Log. Methods Comput. Sci. 11(3) (2015)","DOI":"10.2168\/LMCS-11(3:12)2015"},{"key":"16_CR17","unstructured":"Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. In: Proceedings of STACS. LIPIcs, vol. 66, pp. 30:1\u201330:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proceedings of FOCS, pp. 531\u2013542. IEEE Computer Society (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"16_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems - Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer, New York (1995). \nhttps:\/\/doi.org\/10.1007\/978-1-4612-4222-2"},{"key":"16_CR20","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of FOCS, pp. 746\u2013757. IEEE Computer Society (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"issue":"4","key":"16_CR22","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"EL Post","year":"1946","unstructured":"Post, E.L.: A variant of a recursively unsolvable problem. Bull. Am. Math. Soc. 52(4), 264\u2013268 (1946)","journal-title":"Bull. Am. Math. Soc."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T18:40:22Z","timestamp":1532112022000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}