{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,14]],"date-time":"2026-08-14T10:15:22Z","timestamp":1786702522208,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961446","type":"print"},{"value":"9783319961453","type":"electronic"}],"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_8","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T22:25:55Z","timestamp":1532125555000},"page":"144-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":31,"title":["Model Checking Quantitative Hyperproperties"],"prefix":"10.1007","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christopher","family":"Hahn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hazem","family":"Torfah","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/JCS-2011-0433","volume":"20","author":"MS Alvim","year":"2012","unstructured":"Alvim, M.S., Andr\u00e9s, M.E., Palamidessi, C.: Quantitative information flow in interactive systems. J. Comput. Secur. 20(1), 3\u201350 (2012)","journal-title":"J. Comput. Secur."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Aziz, R.A., Chu, G., Muise, C.J., Stuckey, P.J.: #$$\\exists $$\u2203sat: projected model counting. In: Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing - SAT 2015, Austin, TX, USA, 24\u201327 September 2015, pp. 121\u2013137 (2015)","DOI":"10.1007\/978-3-319-24318-4_10"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Backes, M., K\u00f6pf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: 30th IEEE Symposium on Security and Privacy (S&P 2009), Oakland, California, USA, 17\u201320 May 2009, pp. 141\u2013153 (2009)","DOI":"10.1109\/SP.2009.18"},{"key":"8_CR4","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)"},{"issue":"2","key":"8_CR5","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"15","author":"A Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: Stack-based access control and secure information flow. J. Funct. Program. 15(2), 131\u2013177 (2005)","journal-title":"J. Funct. Program."},{"issue":"6","key":"8_CR6","doi-asserted-by":"crossref","first-page":"1207","DOI":"10.1017\/S0960129511000193","volume":"21","author":"G Barthe","year":"2011","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207\u20131252 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"5","key":"8_CR7","first-page":"481","volume":"10","author":"V Bindschaedler","year":"2017","unstructured":"Bindschaedler, V., Shokri, R., Gunter, C.A.: Plausible deniability for privacy-preserving data synthesis. PVLDB 10(5), 481\u2013492 (2017)","journal-title":"PVLDB"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"702","DOI":"10.1007\/978-3-642-39799-8_49","volume-title":"Computer Aided Verification","author":"F Biondi","year":"2013","unstructured":"Biondi, F., Legay, A., Traonouez, L.-M., W\u0105sowski, A.: QUAIL: a quantitative security analyzer for imperative code. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 702\u2013707. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_49"},{"key":"8_CR9","unstructured":"Chadha, R., Mathur, U., Schwoon, S.: Computing information flow using symbolic model-checking. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, New Delhi, India, 15\u201317 December 2014, pp. 505\u2013516 (2014)"},{"issue":"3","key":"8_CR10","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1515\/popets-2017-0035","volume":"2017","author":"A Chakraborti","year":"2017","unstructured":"Chakraborti, A., Chen, C., Sion, R.: Datalair: efficient block storage with plausible deniability against multi-snapshot adversaries. PoPETs 2017(3), 179 (2017)","journal-title":"PoPETs"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Chen, H., Malacaria, P.: Quantitative analysis of leakage for multi-threaded programs. In: Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security, PLAS 2007, San Diego, California, USA, 14 June 2007, pp. 31\u201340 (2007)","DOI":"10.1145\/1255329.1255335"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-11212-1_13","volume-title":"Computer Security - ESORICS 2014","author":"T Chothia","year":"2014","unstructured":"Chothia, T., Kawamoto, Y., Novakovic, C.: LeakWatch: estimating information leakage from Java programs. In: Kuty\u0142owski, M., Vaidya, J. (eds.) ESORICS 2014. LNCS, vol. 8713, pp. 219\u2013236. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11212-1_13"},{"key":"8_CR13","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/j.entcs.2004.01.018","volume":"112","author":"D Clark","year":"2005","unstructured":"Clark, D., Hunt, S., Malacaria, P.: Quantified interference for a while language. Electr. Notes Theor. Comput. Sci. 112, 149\u2013166 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2","key":"8_CR14","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1093\/logcom\/exi009","volume":"15","author":"D Clark","year":"2005","unstructured":"Clark, D., Hunt, S., Malacaria, P.: Quantitative information flow, relations and polymorphic types. J. Log. Comput. 15(2), 181\u2013199 (2005)","journal-title":"J. Log. Comput."},{"issue":"3","key":"8_CR15","doi-asserted-by":"crossref","first-page":"321","DOI":"10.3233\/JCS-2007-15302","volume":"15","author":"D Clark","year":"2007","unstructured":"Clark, D., Hunt, S., Malacaria, P.: A static analysis for quantifying information flow in a simple imperative language. J. Comput. Secur. 15(3), 321\u2013371 (2007)","journal-title":"J. Comput. Secur."},{"issue":"1","key":"8_CR16","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"8_CR17","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"},{"key":"8_CR18","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). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Myers, A.C., Schneider, F.B.: Belief in information flow. In: 18th IEEE Computer Security Foundations Workshop, (CSFW-18 2005), Aix-en-Provence, France, 20\u201322 June 2005, pp. 31\u201345 (2005)","DOI":"10.1109\/CSFW.2005.10"},{"issue":"5","key":"8_CR20","doi-asserted-by":"crossref","first-page":"655","DOI":"10.3233\/JCS-2009-0353","volume":"17","author":"MR Clarkson","year":"2009","unstructured":"Clarkson, M.R., Myers, A.C., Schneider, F.B.: Quantifying information flow with beliefs. J. Comput. Secur. 17(5), 655\u2013701 (2009)","journal-title":"J. Comput. Secur."},{"issue":"6","key":"8_CR21","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":"8_CR22","unstructured":"Cohen, E.S.: Information transmission in sequential programs. In: Foundations of Secure Computation, pp. 297\u2013335 (1978)"},{"key":"8_CR23","unstructured":"Darwiche, A.: New advances in compiling CNF into decomposable negation normal form. In: Proceedings of the 16th European Conference on Artificial Intelligence, ECAI 2004, including Prestigious Applicants of Intelligent Systems, PAIS 2004, Valencia, Spain, 22\u201327 August 2004, pp. 328\u2013332 (2004)"},{"key":"8_CR24","volume-title":"Cryptography and Data Security","author":"DE Denning","year":"1982","unstructured":"Denning, D.E.: Cryptography and Data Security. Addison-Wesley, Boston (1982)"},{"key":"8_CR25","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). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_12"},{"key":"8_CR26","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). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-319-04921-2_29","volume-title":"Language and Automata Theory and Applications","author":"B Finkbeiner","year":"2014","unstructured":"Finkbeiner, B., Torfah, H.: Counting models of linear-time temporal logic. In: Dediu, A.-H., Mart\u00edn-Vide, C., Sierra-Rodr\u00edguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 360\u2013371. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-04921-2_29"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-319-68167-2_10","volume-title":"Automated Technology for Verification and Analysis","author":"B Finkbeiner","year":"2017","unstructured":"Finkbeiner, B., Torfah, H.: The density of linear-time properties. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 139\u2013155. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_10"},{"key":"8_CR29","unstructured":"Fremont, D.J., Rabe, M.N., Seshia, S.A.: Maximum model counting. In: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, San Francisco, California, USA, 4\u20139 February 2017, pp. 3885\u20133892 (2017)"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Gray III, J.W.: Toward a mathematical foundation for information flow security. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 210\u2013234, May 1991","DOI":"10.1109\/RISP.1991.130769"},{"issue":"6","key":"8_CR31","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"C Hammer","year":"2009","unstructured":"Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Secur. 8(6), 399\u2013422 (2009)","journal-title":"Int. J. Inf. Secur."},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Gray III, J.W.: Toward a mathematical foundation for information flow security. In: IEEE Symposium on Security and Privacy, pp. 21\u201335 (1991)","DOI":"10.1109\/RISP.1991.130769"},{"key":"8_CR33","unstructured":"Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 1997, Providence, Rhode Island, 27\u201331 July 1997, pp. 203\u2013208 (1997)"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"K\u00f6pf, B., Basin, D.A.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings of the 2007 ACM Conference on Computer and Communications Security, CCS 2007, Alexandria, Virginia, USA, 28\u201331 October 2007, pp. 286\u2013296 (2007)","DOI":"10.1145\/1315245.1315282"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"K\u00f6pf, B., Rybalchenko, A.: Approximation and randomization for quantitative information-flow analysis. In: Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, 17\u201319 July 2010, pp. 3\u201314 (2010)","DOI":"10.1109\/CSF.2010.8"},{"issue":"3","key":"8_CR36","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1023\/A:1017584715408","volume":"27","author":"ML Littman","year":"2001","unstructured":"Littman, M.L., Majercik, S.M., Pitassi, T.: Stochastic boolean satisfiability. J. Autom. Reason. 27(3), 251\u2013296 (2001)","journal-title":"J. Autom. Reason."},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Malacaria, P.: Assessing security threats of looping constructs. In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, 17\u201319 January 2007, pp. 225\u2013235 (2007)","DOI":"10.1145\/1190216.1190251"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-41488-6_17","volume-title":"Secure IT Systems","author":"D Milushev","year":"2013","unstructured":"Milushev, D., Clarke, D.: Incremental hyperproperty model checking via games. In: Riis Nielson, H., Gollmann, D. (eds.) NordSec 2013. LNCS, vol. 8208, pp. 247\u2013262. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41488-6_17"},{"issue":"3","key":"8_CR39","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on $$\\omega $$\u03c9-words. Theoret. Comput. Sci. 32(3), 321\u2013330 (1984)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR40","unstructured":"Morwood, D., Bryce, D.: Evaluating temporal plans in incomplete domains. In: Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 22\u201326 July 2012, Toronto, Ontario, Canada (2012)"},{"key":"8_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-30353-1_36","volume-title":"Advances in Artificial Intelligence","author":"CJ Muise","year":"2012","unstructured":"Muise, C.J., McIlraith, S.A., Beck, J.C., Hsu, E.I.: Dsharp: fast d-DNNF compilation with sharpSAT. In: Kosseim, L., Inkpen, D. (eds.) AI 2012. LNCS (LNAI), vol. 7310, pp. 356\u2013361. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30353-1_36"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: JFlow: practical mostly-static information flow control. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1999, San Antonio, TX, USA, 20\u201322 January 1999, pp. 228\u2013241 (1999)","DOI":"10.1145\/292540.292561"},{"key":"8_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-642-00596-1_21","volume-title":"Foundations of Software Science and Computational Structures","author":"G Smith","year":"2009","unstructured":"Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 288\u2013302. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_21"},{"issue":"3","key":"8_CR44","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s00236-016-0284-z","volume":"55","author":"H Torfah","year":"2016","unstructured":"Torfah, H., Zimmermann, M.: The complexity of counting models of linear-time temporal logic. Acta Informatica 55(3), 191\u2013212 (2016)","journal-title":"Acta Informatica"},{"key":"8_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-15497-3_22","volume-title":"Computer Security \u2013 ESORICS 2010","author":"H Yasuoka","year":"2010","unstructured":"Yasuoka, H., Terauchi, T.: On bounding problems of quantitative information flow. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 357\u2013372. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15497-3_22"},{"key":"8_CR46","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/j.tcs.2013.07.031","volume":"538","author":"H Yasuoka","year":"2014","unstructured":"Yasuoka, H., Terauchi, T.: Quantitative information flow as safety and liveness hyperproperties. Theor. Comput. Sci. 538, 167\u2013182 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR47","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings of CSF, p. 29. IEEE Computer Society (2003)","DOI":"10.1109\/CSFW.2003.1212703"}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,28]],"date-time":"2022-08-28T00:39:30Z","timestamp":1661647170000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}