{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T13:17:36Z","timestamp":1758633456863,"version":"3.40.3"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030532871"},{"type":"electronic","value":"9783030532888"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53288-8_11","type":"book-chapter","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T19:03:27Z","timestamp":1594839807000},"page":"201-224","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Verification of Quantitative Hyperproperties Using Trace Enumeration Relations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3434-6937","authenticated-orcid":false,"given":"Shubham","family":"Sahai","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2288-3396","authenticated-orcid":false,"given":"Pramod","family":"Subramanyan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9107-0239","authenticated-orcid":false,"given":"Rohit","family":"Sinha","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-662-52993-5_9","volume-title":"Fast Software Encryption","author":"JB Almeida","year":"2016","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F.: Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. In: Peyrin, T. (ed.) FSE 2016. LNCS, vol. 9783, pp. 163\u2013184. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-52993-5_9"},{"key":"11_CR2","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: 25th USENIX Security Symposium, USENIX Security, pp. 53\u201370 (2016)"},{"issue":"1","key":"11_CR3","doi-asserted-by":"publisher","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":"11_CR4","doi-asserted-by":"crossref","unstructured":"Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T., Wei, S.: Decomposition instead of self-composition for proving the absence of timing channels. In: PLDI, pp. 362\u2013375 (2017)","DOI":"10.1145\/3140587.3062378"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T., Wei, S.: Decomposition instead of self-composition for proving the absence of timing channels. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, New York, NY, USA, pp. 362\u2013375. ACM (2017)","DOI":"10.1145\/3062341.3062378"},{"issue":"7","key":"11_CR6","doi-asserted-by":"publisher","first-page":"796","DOI":"10.1016\/j.scico.2011.10.008","volume":"78","author":"JB Almeida","year":"2013","unstructured":"Almeida, J.B., Barbosa, M., Pinto, J.S., Vieira, B.: Formal verification of side-channel countermeasures using self-composition. Sci. Comput. Program. 78(7), 796\u2013812 (2013)","journal-title":"Sci. Comput. Program."},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Backes, M., Kopf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: Proceedings of the 2009 30th IEEE Symposium on Security and Privacy, SP 2009, Washington, DC, USA, pp. 141\u2013153. IEEE Computer Society (2009)","DOI":"10.1109\/SP.2009.18"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Barthe, G., Betarte, G., Campo, J., Luna, C., Pichardie, D.: System-level non-interference for constant-time cryptography. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp. 1267\u20131279. ACM (2014)","DOI":"10.1145\/2660267.2660283"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200\u2013214. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17"},{"key":"11_CR10","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: 17th IEEE Computer Security Foundations Workshop (CSFW-17), pp. 100\u2013114 (2004)"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Barthe, G., Hsu, J., Liao, K.: A probabilistic separation logic. In: Proceedings of ACM Programming Language, vol. 4, no. POPL, December 2019","DOI":"10.1145\/3371123"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Bindschaedler, V., Shokri, R., Gunter, C.A.: Plausible deniability for privacy-preserving data synthesis. In: Proceedings of the VLDB Endowment, vol. 10, no. 5, pp. 481\u2013492 (2017)","DOI":"10.14778\/3055540.3055542"},{"key":"11_CR13","unstructured":"Bj\u00f6rner, A., Stanley, R.P.: A Combinatorial Miscellany. L\u2019Enseignement math\u00e9matique (2010)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Chakraborti, A., Chen, C., Sion, R.: Datalair: efficient block storage with plausible deniability against multi-snapshot adversaries. In: Proceedings on Privacy Enhancing Technologies, vol. 2017, no. 3, pp. 179\u2013197 (2017)","DOI":"10.1515\/popets-2017-0035"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Cheang, K., Rasmussen, C., Seshia, S., Subramanyan, P.: A formal approach to secure speculation. In: 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), pp. 288\u201328815, June 2019","DOI":"10.1109\/CSF.2019.00027"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Chen, J., Feng, Y., Dillig, I.: Precise detection of side-channel vulnerabilities using quantitative cartesian hoare logic. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, New York, NY, USA, pp. 875\u2013890. ACM (2017)","DOI":"10.1145\/3133956.3134058"},{"issue":"2","key":"11_CR17","doi-asserted-by":"publisher","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. Logic Comput. 15(2), 181\u2013199 (2005)","journal-title":"J. Logic Comput."},{"issue":"3","key":"11_CR18","doi-asserted-by":"publisher","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."},{"key":"11_CR19","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":"11_CR20","unstructured":"Clarkson, M.R., Myers, A.C., Schneider, F.B.: Belief in information flow. In: 18th IEEE Computer Security Foundations Workshop (CSFW 2005), pp. 31\u201345. IEEE (2005)"},{"issue":"6","key":"11_CR21","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":"11_CR22","doi-asserted-by":"crossref","unstructured":"Darais, D., Sweet, I., Liu, C., Hicks, M.: A language for probabilistically oblivious computation. In: Proceedings of ACM Programming Language, vol. 4, no. POPL, December 2019","DOI":"10.1145\/3371118"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"7","key":"11_CR24","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504\u2013513 (1977)","journal-title":"Commun. ACM"},{"key":"11_CR25","unstructured":"Experiments: Models and Proof Scripts for the paper Verification of Quantitative Hyperproperties Using Trace Enumeration Relations (2020). https:\/\/github.com\/ssahai\/CAV-2020-benchmarks"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Farzan, A., Vandikas, A.: Automated hypersafety verification. In: Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, 15\u201318 July 2019, Proceedings, Part I, pp. 200\u2013218 (2019)","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-030-25540-4_14","volume-title":"Computer Aided Verification","author":"G Fedyukovich","year":"2019","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 259\u2013277. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Ferraiuolo, A., Xu, R., Zhang, D., Myers, A.C., Suh, G.E.: Verification of a practical hardware security architecture through static information flow analysis. In: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2017, Xi\u2019an, China, 8\u201312 April 2017, pp. 555\u2013568 (2017)","DOI":"10.1145\/3037697.3037739"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Hahn, C., Torfah, H.: Model checking quantitative hyperproperties. In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, 14\u201317 July 2018, Proceedings, Part I, pp. 144\u2013163 (2018)","DOI":"10.1007\/978-3-319-96145-3_8"},{"key":"11_CR30","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$$^*$$. 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":"11_CR31","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Rabe, M.N., Seshia, S.A.: Maximum model counting. In: Thirty-First AAAI Conference on Artificial Intelligence (2017)","DOI":"10.1609\/aaai.v31i1.11138"},{"key":"11_CR32","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, 26\u201328 April 1982, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"issue":"3","key":"11_CR33","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/233551.233553","volume":"43","author":"O Goldreich","year":"1996","unstructured":"Goldreich, O., Ostrovsky, R.: Software protection and simulation on oblivious rams. J. ACM 43(3), 431\u2013473 (1996)","journal-title":"J. ACM"},{"issue":"3\u20134","key":"11_CR34","first-page":"255","volume":"1","author":"W James","year":"1992","unstructured":"James, W., Gray, I.I.I.: Toward a mathematical foundation for information flow security. J.Comput. Secur. 1(3\u20134), 255\u2013294 (1992)","journal-title":"J.Comput. Secur."},{"key":"11_CR35","unstructured":"Guarnieri, M., Morales, B.J.F., Reineke, J., S\u00e1nchez, A.: SPECTECTOR: principled detection of speculative information flows. CoRR, abs\/1812.08639 (2018)"},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-030-01090-4_15","volume-title":"Automated Technology for Verification and Analysis","author":"A Gurfinkel","year":"2018","unstructured":"Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 248\u2013266. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_15"},{"key":"11_CR37","unstructured":"Hawblitzel, C., et al.: Ironclad apps: end-to-end security via automated full-system verification. In: Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, pp. 165\u2013181 (2014)"},{"key":"11_CR38","doi-asserted-by":"publisher","unstructured":"K\u00f6pf, B., Mauborgne, L., Ochoa, M.: Automatic quantification of cache side-channels. In: International Conference on Computer Aided Verification, pp. 564\u2013580. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_40","DOI":"10.1007\/978-3-642-31424-7_40"},{"key":"11_CR39","doi-asserted-by":"crossref","unstructured":"Muduli, S.K., Subramanyan, P., Ray, S.: Verification of authenticated firmware loaders. In: Proceedings of Formal Methods in Computer-Aided Design. IEEE (2019)","DOI":"10.23919\/FMCAD.2019.8894262"},{"key":"11_CR40","unstructured":"Ren, L., et al.: Constants count: practical improvements to oblivious RAM. In: 24th USENIX Security Symposium (USENIX Security 15), Washington, D.C., pp. 415\u2013430, August 2015. USENIX Association (2015)"},{"key":"11_CR41","unstructured":"Roscoe, A.W.: CSP and determinism in security modelling. In: Proceedings of the 1995 IEEE Symposium on Security and Privacy, Oakland, California, USA, 8\u201310 May 1995, pp. 114\u2013127 (1995)"},{"key":"11_CR42","doi-asserted-by":"crossref","unstructured":"Rushby, J.M.: Proof of separability: a verification technique for a class of a security kernels. In: International Symposium on Programming, 5th Colloquium, Torino, Italy, 6\u20138 April 1982, Proceedings, pp. 352\u2013367 (1982)","DOI":"10.1007\/3-540-11494-7_23"},{"key":"11_CR43","doi-asserted-by":"crossref","unstructured":"Sahai, S., Subramanyan, P., Sinha, R.: Verification of quantitative hyperproperties using trace enumeration relations. arXiv e-prints arXiv:abs\/2005.04606 , May 2020","DOI":"10.1007\/978-3-030-53288-8_11"},{"key":"11_CR44","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Subramanyan, P.: Uclid 5: integrating modeling, verification, synthesis and learning. In: Proceedings of the 16th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), October 2018","DOI":"10.1109\/MEMCOD.2018.8556946"},{"key":"11_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-030-25540-4_9","volume-title":"Computer Aided Verification","author":"R Shemer","year":"2019","unstructured":"Shemer, R., Gurfinkel, A., Shoham, S., Vizel, Y.: Property directed self composition. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 161\u2013179. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_9"},{"key":"11_CR46","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"},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"Sousa, M., Dillig, I.: Cartesian hoare logic for verifying k-safety properties. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, New York, NY, USA, pp. 57\u201369. ACM (2016)","DOI":"10.1145\/2908080.2908092"},{"key":"11_CR48","doi-asserted-by":"crossref","unstructured":"Stefanov, E., et al.: Path ORAM: an extremely simple oblivious RAM protocol. In: 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013, Berlin, Germany, 4\u20138 November 2013, pp. 299\u2013310 (2013)","DOI":"10.1145\/2508859.2516660"},{"key":"11_CR49","doi-asserted-by":"crossref","unstructured":"Subramanyan, P., Sinha, R., Lebedev, I.A., Devadas, S., Seshia, S.A.: A formal foundation for secure remote execution of enclaves. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, 30 October\u201303 November 2017, pp. 2435\u20132450 (2017)","DOI":"10.1145\/3133956.3134098"},{"key":"11_CR50","doi-asserted-by":"crossref","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Static Analysis, 12th International Symposium, SAS, Proceedings, pp. 352\u2013367 (2005)","DOI":"10.1007\/11547662_24"},{"key":"11_CR51","unstructured":"UCLID5 Verification and Synthesis System (2019). http:\/\/github.com\/uclid-org\/uclid\/"},{"key":"11_CR52","doi-asserted-by":"crossref","unstructured":"Wilf, H.S.: Generatingfunctionology. AK Peters\/CRC Press (2005)","DOI":"10.1201\/b10576"},{"key":"11_CR53","doi-asserted-by":"crossref","unstructured":"Yang, W., Subramanyan, P., Vizel, Y., Gupta, A., Malik, S.: Lazy self-composition for security verification. In: Computer Aided Verification - 30th International Conference, CAV 2018, Oxford, UK, 14\u201317 July 2018, Proceedings (2018)","DOI":"10.1007\/978-3-319-96142-2_11"},{"key":"11_CR54","doi-asserted-by":"publisher","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":"11_CR55","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings of the 16th IEEE Computer Security Foundations Workshop, pp. 29\u201343. IEEE (2003)"},{"key":"11_CR56","doi-asserted-by":"crossref","unstructured":"Zeilberger, D.: Enumerative and algebraic combinatorics. In: The Princeton Companion to Mathematics, pp. 550\u2013561. Princeton University Press (2010)","DOI":"10.1515\/9781400830398.550"},{"key":"11_CR57","doi-asserted-by":"crossref","unstructured":"Zhang, D., Wang, Y., Edward Suh, G., Myers, A.C.: A hardware design language for timing-sensitive information-flow security. In: Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2015, Istanbul, Turkey, 14\u201318 March 2015, pp. 503\u2013516 (2015)","DOI":"10.1145\/2694344.2694372"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53288-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,2]],"date-time":"2022-11-02T22:00:43Z","timestamp":1667426443000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-53288-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030532871","9783030532888"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53288-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair.org","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"240","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}