{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:27:42Z","timestamp":1757312862616,"version":"3.40.3"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131844"},{"type":"electronic","value":"9783031131851"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"Abstract<\/jats:title>Quantified information flow (QIF) has emerged as a rigorous approach to quantitatively measure confidentiality; the information-theoretic underpinning of QIF allows the end-users to link the computed quantities with the computational effort required on the part of the adversary to gain access to desired confidential information. In this work, we focus on the estimation of Shannon entropy for a given program $$\\varPi $$<\/jats:tex-math>\n \u03a0<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. As a first step, we focus on the case wherein a Boolean formula $$\\varphi (X,Y)$$<\/jats:tex-math>\n \n \u03c6<\/mml:mi>\n (<\/mml:mo>\n X<\/mml:mi>\n ,<\/mml:mo>\n Y<\/mml:mi>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> captures the relationship between inputs X<\/jats:italic> and output Y<\/jats:italic> of $$\\varPi $$<\/jats:tex-math>\n \u03a0<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Such formulas $$\\varphi (X,Y)$$<\/jats:tex-math>\n \n \u03c6<\/mml:mi>\n (<\/mml:mo>\n X<\/mml:mi>\n ,<\/mml:mo>\n Y<\/mml:mi>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> have the property that for every valuation to X<\/jats:italic>, there exists exactly one valuation to Y<\/jats:italic> such that $$\\varphi $$<\/jats:tex-math>\n \u03c6<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is satisfied. The existing techniques require $$\\mathcal {O}(2^m)$$<\/jats:tex-math>\n \n O<\/mml:mi>\n (<\/mml:mo>\n \n 2<\/mml:mn>\n m<\/mml:mi>\n <\/mml:msup>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> model counting queries, where $$m = |Y|$$<\/jats:tex-math>\n \n m<\/mml:mi>\n =<\/mml:mo>\n |<\/mml:mo>\n Y<\/mml:mi>\n |<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p>We propose the first efficient algorithmic technique, called $$\\mathsf {EntropyEstimation}$$<\/jats:tex-math>\n EntropyEstimation<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> to estimate the Shannon entropy of $$\\varphi $$<\/jats:tex-math>\n \u03c6<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> with PAC-style guarantees, i.e., the computed estimate is guaranteed to lie within a $$(1\\pm \\varepsilon )$$<\/jats:tex-math>\n \n (<\/mml:mo>\n 1<\/mml:mn>\n \u00b1<\/mml:mo>\n \u03b5<\/mml:mi>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-factor of the ground truth with confidence at least $$1-\\delta $$<\/jats:tex-math>\n \n 1<\/mml:mn>\n -<\/mml:mo>\n \u03b4<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Furthermore, $$\\mathsf {EntropyEstimation}$$<\/jats:tex-math>\n EntropyEstimation<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> makes only $$\\mathcal {O}(\\frac{min(m,n)}{\\varepsilon ^2})$$<\/jats:tex-math>\n \n O<\/mml:mi>\n (<\/mml:mo>\n \n \n m<\/mml:mi>\n i<\/mml:mi>\n n<\/mml:mi>\n (<\/mml:mo>\n m<\/mml:mi>\n ,<\/mml:mo>\n n<\/mml:mi>\n )<\/mml:mo>\n <\/mml:mrow>\n \n \u03b5<\/mml:mi>\n 2<\/mml:mn>\n <\/mml:msup>\n <\/mml:mfrac>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> counting and sampling queries, where $$m = |Y|$$<\/jats:tex-math>\n \n m<\/mml:mi>\n =<\/mml:mo>\n |<\/mml:mo>\n Y<\/mml:mi>\n |<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, and $$n = |X|$$<\/jats:tex-math>\n \n n<\/mml:mi>\n =<\/mml:mo>\n |<\/mml:mo>\n X<\/mml:mi>\n |<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, thereby achieving a significant reduction in the number of model counting queries. We demonstrate the practical efficiency of our algorithmic framework via a detailed experimental evaluation. Our evaluation demonstrates that the proposed framework scales to the formulas beyond the reach of the previously known approaches.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_18","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"363-384","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Scalable Shannon Entropy Estimator"],"prefix":"10.1007","author":[{"given":"Priyanka","family":"Golia","sequence":"first","affiliation":[]},{"given":"Brendan","family":"Juba","sequence":"additional","affiliation":[]},{"given":"Kuldeep S.","family":"Meel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"18_CR1","unstructured":"QBF solver evaluation portal 2017. http:\/\/www.qbflib.org\/qbfeval17.php"},{"key":"18_CR2","unstructured":"QBF solver evaluation portal 2018. http:\/\/www.qbflib.org\/qbfeval18.php"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-94144-8_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"D Achlioptas","year":"2018","unstructured":"Achlioptas, D., Hammoudeh, Z.S., Theodoropoulos, P.: Fast sampling of perfectly uniform satisfying assignments. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 135\u2013147. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_9"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-21690-4_15","volume-title":"Computer Aided Verification","author":"A Aydin","year":"2015","unstructured":"Aydin, A., Bang, L., Bultan, T.: Automata-based model counting for string constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 255\u2013272. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_15"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Aydin, A., et al.: Parameterized model counting for string and numeric constraints. In: Proceedings of ESEC\/FSE, pp. 400\u2013410 (2018)","DOI":"10.1145\/3236024.3236064"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-24318-4_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"RA Aziz","year":"2015","unstructured":"Aziz, R.A., Chu, G., Muise, C., Stuckey, P.: $$\\#\\exists $$SAT: projected model counting. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 121\u2013137. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_10"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Backes, M., K\u00f6pf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: Proceedings of SP (2009)","DOI":"10.1109\/SP.2009.18"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Bang, L., Aydin, A., Phan, Q.S., P\u0103s\u0103reanu, C.S., Bultan, T.: String analysis for side channels with segmented oracles. In: Proceedings of SIGSOFT (2016)","DOI":"10.1145\/2950290.2950362"},{"issue":"1","key":"18_CR9","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1137\/S0097539702403645","volume":"35","author":"T Batu","year":"2005","unstructured":"Batu, T., Dasgupta, S., Kumar, R., Rubinfeld, R.: The complexity of approximating the entropy. SIAM J. Comput. 35(1), 132\u2013150 (2005)","journal-title":"SIAM J. Comput."},{"key":"18_CR10","unstructured":"Bayardo Jr, R.J., Pehoushek, J.D.: Counting models using connected components. In: AAAI\/IAAI, pp. 157\u2013162 (2000)"},{"key":"18_CR11","unstructured":"Bevier, W.R., Cohen, R.M., Young, W.D.: Connection policies and controlled interference. In: Proceedings of CSF (1995)"},{"key":"18_CR12","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1613\/jair.601","volume":"10","author":"E Birnbaum","year":"1999","unstructured":"Birnbaum, E., Lozinskii, E.L.: The good old Davis-Putnam procedure helps counting models. J. Artif. Intell. Res. 10, 457\u2013477 (1999)","journal-title":"J. Artif. Intell. Res."},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-57288-8_9","volume-title":"NASA Formal Methods","author":"M Borges","year":"2017","unstructured":"Borges, M., Phan, Q.-S., Filieri, A., P\u0103s\u0103reanu, C.S.: Model-counting approaches for nonlinear numerical constraints. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 131\u2013138. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_9"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-030-41600-3_3","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"T Bultan","year":"2020","unstructured":"Bultan, T.: Quantifying information leakage using model counting constraint solvers. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 30\u201335. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_3"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Canonne, C.L.: A survey on distribution testing: your data is big. But is it blue? Theory Comput. 1\u2013100 (2020)","DOI":"10.4086\/toc.gs.2020.009"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Cern\u1ef3, P., Chatterjee, K., Henzinger, T.A.: The complexity of quantitative information flow problems. In: Proceedings of CSF (2011)","DOI":"10.1109\/CSF.2011.21"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Fischer, E., Goldhirsh, Y., Matsliah, A.: On the power of conditional samples in distribution testing. SIAM J. Comput. (2016)","DOI":"10.1137\/140964199"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: Distribution-aware sampling and weighted model counting for SAT, In: AAAI, pp. 1722\u20131730. AAAI Press (2014)","DOI":"10.1609\/aaai.v28i1.8990"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Balancing scalability and uniformity in SAT witness generator. In: Proceedings of DAC (2014)","DOI":"10.1145\/2593069.2593097"},{"key":"18_CR20","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Algorithmic improvements in approximate counting for probabilistic inference: from linear to logarithmic sat calls. In: IJCAI (2016)"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Chen, S., Wang, R., Wang, X., Zhang, K.: Side-channel leaks in web applications: a reality today, a challenge tomorrow. In: Proceedings of SP (2010)","DOI":"10.1109\/SP.2010.20"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Cherubin, G., Chatzikokolakis, K., Palamidessi, C.: F-BLEAU: fast black-box leakage estimation. In: Proceedings of SP (2019)","DOI":"10.1109\/SP.2019.00073"},{"key":"18_CR23","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":"18_CR24","doi-asserted-by":"crossref","unstructured":"Clark, D., Hunt, S., Malacaria, P.: A static analysis for quantifying information flow in a simple imperative language. J. Comput. Secur. (2007)","DOI":"10.3233\/JCS-2007-15302"},{"issue":"1\u20132","key":"18_CR25","doi-asserted-by":"publisher","first-page":"11","DOI":"10.3166\/jancl.11.11-34","volume":"11","author":"A Darwiche","year":"2001","unstructured":"Darwiche, A.: On the tractable counting of theory models and its application to truth maintenance and belief revision. J. Appl. Non-Classical Logics 11(1\u20132), 11\u201334 (2001)","journal-title":"J. Appl. Non-Classical Logics"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Denning, D.E.: A lattice model of secure information flow. Commun. ACM (1976)","DOI":"10.1145\/360051.360056"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Eiers, W., Saha, S., Brennan, T., Bultan, T.: Subformula caching for model counting and quantitative program analysis. In: 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 453\u2013464. IEEE (2019)","DOI":"10.1109\/ASE.2019.00050"},{"issue":"2","key":"18_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2685616","volume":"24","author":"H Eldib","year":"2014","unstructured":"Eldib, H., Wang, C., Schaumont, P.: Formal verification of software countermeasures against side-channel attacks. ACM Trans. Softw. Eng. Methodol. (TOSEM) 24(2), 1\u201324 (2014)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Eldib, H., Wang, C., Taha, M., Schaumont, P.: QMS: evaluating the side-channel resistance of masked software from source code. In: 2014 51st ACM\/EDAC\/IEEE Design Automation Conference (DAC), pp. 1\u20136. IEEE (2014)","DOI":"10.1109\/DAC.2014.6881536"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Ferrari, E., Samarati, P., Bertino, E., Jajodia, S.: Providing flexibility in information flow control for object oriented systems. In: Proceedings of SP (1997)","DOI":"10.1109\/69.617048"},{"key":"18_CR31","doi-asserted-by":"crossref","unstructured":"Fichte, J.K., Hecher, M., Hamiti, F.: The model counting competition 2020. arXiv preprint arXiv:2012.01323 (2020). https:\/\/arxiv.org\/pdf\/2012.01323.pdf","DOI":"10.1145\/3459080"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Fremont, D., Rabe, M., Seshia, S.: Maximum model counting. In: Proceedings of AAAI (2017)","DOI":"10.1609\/aaai.v31i1.11138"},{"issue":"3","key":"18_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3330392","volume":"28","author":"P Gao","year":"2019","unstructured":"Gao, P., Zhang, J., Song, F., Wang, C.: Verifying and quantifying side-channel resistance of masked software implementations. ACM Trans. Softw. Eng. Methodol. (TOSEM) 28(3), 1\u201332 (2019)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"18_CR34","unstructured":"Goldreich, O., Vadhan, S.: Comparing entropies in statistical zero knowledge with applications to the structure of SZK. In: Proceedings of CCC, pp. 54\u201373. IEEE (1999)"},{"issue":"4","key":"18_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1597036.1597038","volume":"5","author":"S Guha","year":"2009","unstructured":"Guha, S., McGregor, A., Venkatasubramanian, S.: Sublinear estimation of entropy and information distances. ACM Trans. Algorithms (TALG) 5(4), 1\u201316 (2009)","journal-title":"ACM Trans. Algorithms (TALG)"},{"key":"18_CR36","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1613\/jair.2097","volume":"29","author":"J Huang","year":"2007","unstructured":"Huang, J., Darwiche, A.: The language of search. J. Artif. Intell. Res. 29, 191\u2013219 (2007)","journal-title":"J. Artif. Intell. Res."},{"key":"18_CR37","doi-asserted-by":"crossref","unstructured":"Kadron, \u0130.B., Rosner, N., Bultan, T.: Feedback-driven side-channel analysis for networked applications. In: Proceedings of SIGSOFT (2020)","DOI":"10.1145\/3395363.3397365"},{"key":"18_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-319-89960-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kim","year":"2018","unstructured":"Kim, S., McCamant, S.: Bit-vector model counting using statistical estimation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 133\u2013151. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_8"},{"key":"18_CR39","unstructured":"Klebanov, V.: Precise quantitative information flow analysis using symbolic model counting. QASA (2012)"},{"key":"18_CR40","doi-asserted-by":"crossref","unstructured":"K\u00f6pf, B., Basin, D.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings of CCS (2007)","DOI":"10.1145\/1315245.1315282"},{"key":"18_CR41","doi-asserted-by":"crossref","unstructured":"K\u00f6pf, B., Rybalchenko, A.: Approximation and randomization for quantitative information-flow analysis. In: Proceedings of CSF, pp. 3\u201314. IEEE (2010)","DOI":"10.1109\/CSF.2010.8"},{"key":"18_CR42","doi-asserted-by":"crossref","unstructured":"Lagniez, J.M., Marquis, P.: A recursive algorithm for projected model counting. In: Proceedings of AAAI, vol. 33, pp. 1536\u20131543 (2019)","DOI":"10.1609\/aaai.v33i01.33011536"},{"key":"18_CR43","doi-asserted-by":"crossref","unstructured":"Ma, S.K.: Calculation of entropy from data of motion. J. Stat. Phys. 26(2), 221\u2013240 (1981)","DOI":"10.1007\/BF01013169"},{"key":"18_CR44","doi-asserted-by":"crossref","unstructured":"Meng, Z., Smith, G.: Calculating bounds on information leakage using two-bit patterns. In: Proceedings of PLAS (2011)","DOI":"10.1145\/2166956.2166957"},{"key":"18_CR45","doi-asserted-by":"crossref","unstructured":"M\u00f6hle, S., Biere, A.: Dualizing projected model counting. In: Proceedings of ICTAI, pp. 702\u2013709. IEEE (2018)","DOI":"10.1109\/ICTAI.2018.00111"},{"key":"18_CR46","doi-asserted-by":"crossref","unstructured":"Phan, Q.S., Bang, L., Pasareanu, C.S., Malacaria, P., Bultan, T.: Synthesis of adaptive side-channel attacks. In: Proceedings of CSF (2017)","DOI":"10.1109\/CSF.2017.8"},{"key":"18_CR47","doi-asserted-by":"crossref","unstructured":"Phan, Q.S., Malacaria, P.: Abstract model counting: a novel approach for quantification of information leaks. In: Proceedings of CCS (2014)","DOI":"10.1145\/2590296.2590328"},{"key":"18_CR48","doi-asserted-by":"crossref","unstructured":"Phan, Q.S., Malacaria, P., Tkachuk, O., P\u0103s\u0103reanu, C.S.: Symbolic quantitative information flow. Proc. ACM SIGSOFT (2012)","DOI":"10.1145\/2382756.2382791"},{"key":"18_CR49","doi-asserted-by":"crossref","unstructured":"Rosner, N., Kadron, I.B., Bang, L., Bultan, T.: Profit: detecting and quantifying side channels in networked applications. In: Proceedings of NDSS (2019)","DOI":"10.14722\/ndss.2019.23536"},{"key":"18_CR50","unstructured":"Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. SAT 4, 7th (2004)"},{"key":"18_CR51","unstructured":"Sharma, S., Gupta, R., Roy, S., Meel, K.S.: Knowledge compilation meets uniform sampling. In: Proceedings of LPAR (2018)"},{"key":"18_CR52","doi-asserted-by":"crossref","unstructured":"Sharma, S., Roy, S., Soos, M., Meel, K.S.: Ganak: a scalable probabilistic exact model counter. In: Proceedings of IJCAI (2019)","DOI":"10.24963\/ijcai.2019\/163"},{"key":"18_CR53","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":"18_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-030-53288-8_22","volume-title":"Computer Aided Verification","author":"M Soos","year":"2020","unstructured":"Soos, M., Gocht, S., Meel, K.S.: Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 463\u2013484. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_22"},{"issue":"1","key":"18_CR55","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1103\/PhysRevLett.80.197","volume":"80","author":"SP Strong","year":"1998","unstructured":"Strong, S.P., Koberle, R., Van Steveninck, R.R.D.R., Bialek, W.: Entropy and information in neural spike trains. Phys. Rev. Lett. 80(1), 197 (1998)","journal-title":"Phys. Rev. Lett."},{"key":"18_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11814948_38","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"M Thurley","year":"2006","unstructured":"Thurley, M.: sharpSAT \u2013 counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424\u2013429. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_38"},{"key":"18_CR57","doi-asserted-by":"crossref","unstructured":"Val, C.G., Enescu, M.A., Bayless, S., Aiello, W., Hu, A.J.: Precisely measuring quantitative information flow: 10k lines of code and beyond. In: Proceedings of EuroS &P, pp. 31\u201346. IEEE (2016)","DOI":"10.1109\/EuroSP.2016.15"},{"issue":"6","key":"18_CR58","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3125643","volume":"64","author":"G Valiant","year":"2017","unstructured":"Valiant, G., Valiant, P.: Estimating the unseen: improved estimators for entropy and other properties. J. ACM 64(6), 1\u201341 (2017)","journal-title":"J. ACM"},{"key":"18_CR59","doi-asserted-by":"crossref","unstructured":"Zhou, Z., Qian, Z., Reiter, M.K., Zhang, Y.: Static evaluation of noninterference using approximate model counting. In: Proceedings of SP (2018)","DOI":"10.1109\/SP.2018.00052"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T17:13:32Z","timestamp":1667495612000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_18","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":"7 August 2022","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":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","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","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","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":"40","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":"11","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":"19% - 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":"3.9","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":"9.7","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)"}}]}}