{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:37Z","timestamp":1763468137612},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642401954"},{"type":"electronic","value":"9783642401961"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40196-1_16","type":"book-chapter","created":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T01:54:56Z","timestamp":1374544496000},"page":"177-192","source":"Crossref","is-referenced-by-count":32,"title":["SAT-Based Analysis and Quantification of Information Flow in Programs"],"prefix":"10.1007","author":[{"given":"Vladimir","family":"Klebanov","sequence":"first","affiliation":[]},{"given":"Norbert","family":"Manthey","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Muise","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Backes, M., Berg, M., K\u00f6pf, B.: Non-uniform distributions in quantitative information-flow. In: ASIACCS 2011, pp. 367\u2013375. ACM (2011)","DOI":"10.1145\/1966913.1966960"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Backes, M., K\u00f6pf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: S&P 2009, pp. 141\u2013153. IEEE Computer Society (2009)","DOI":"10.1109\/SP.2009.18"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-20398-5_7","volume-title":"NASA Formal Methods","author":"J. Brauer","year":"2011","unstructured":"Brauer, J., King, A.: Approximate quantifier elimination for propositional boolean formulae. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 73\u201388. Springer, Heidelberg (2011)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-22110-1_17","volume-title":"Computer Aided Verification","author":"J. Brauer","year":"2011","unstructured":"Brauer, J., King, A., Kriener, J.: Existential quantification as incremental SAT. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 191\u2013207. Springer, Heidelberg (2011)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-12002-2_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Chatzikokolakis","year":"2010","unstructured":"Chatzikokolakis, K., Chothia, T., Guha, A.: Statistical measurement of information leakage. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 390\u2013404. Springer, Heidelberg (2010)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"issue":"4","key":"16_CR7","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1145\/502090.502091","volume":"48","author":"A. Darwiche","year":"2001","unstructured":"Darwiche, A.: Decomposable negation normal form. J. ACM\u00a048(4), 608\u2013647 (2001)","journal-title":"J. ACM"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Dennis, G., Chang, F.S.-H., Jackson, D.: Modular verification of code with SAT. In: ISSTA 2006, pp. 109\u2013120. ACM (2006)","DOI":"10.1145\/1146238.1146251"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Guo, Q., Sang, J., He, Y.-M.: Effective preprocessing in #SAT. In: ICMV 2011. SPIE (2011)","DOI":"10.1117\/12.921379"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-12459-4_8","volume-title":"Formal Aspects in Security and Trust","author":"J. Heusser","year":"2010","unstructured":"Heusser, J., Malacaria, P.: Applied quantitative information flow and statistical databases. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol.\u00a05983, pp. 96\u2013110. Springer, Heidelberg (2010)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Heusser, J., Malacaria, P.: Quantifying information leaks in software. In: ACSAC 2010, pp. 261\u2013269. ACM (2010)","DOI":"10.1145\/1920261.1920300"},{"key":"16_CR13","unstructured":"Klebanov, V.: Precise quantitative information flow analysis using symbolic model counting. In: Martinelli, F., Nielson, F. (eds.) Proceedings of the International Workshop on Quantitative Aspects in Security Assurance, QASA (2012)"},{"key":"16_CR14","first-page":"3","volume-title":"CSF 2010","author":"B. K\u00f6pf","year":"2010","unstructured":"K\u00f6pf, B., Rybalchenko, A.: Approximation and randomization for quantitative information-flow analysis. In: CSF 2010, pp. 3\u201314. IEEE Computer Society, Washington, DC (2010)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-31612-8_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"N. Manthey","year":"2012","unstructured":"Manthey, N.: Coprocessor 2.0 \u2013 A flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 436\u2013441. Springer, Heidelberg (2012)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Proceedings of Haifa Verification Conference 2012 (2012)","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"McCamant, S., Ernst, M.D.: Quantitative information flow as network flow capacity. In: PLDI 2008, pp. 193\u2013205. ACM (2008)","DOI":"10.1145\/1375581.1375606"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Meng, Z., Smith, G.: Calculating bounds on information leakage using two-bit patterns. In: PLAS 2011, pp. 1\u201312. ACM (2011)","DOI":"10.1145\/2166956.2166957"},{"key":"16_CR19","unstructured":"Mu, C.: Quantitative information flow for security: a survey. Technical Report TR-08-06, Department of Computer Science, King\u2019s College London (2008), \n                    \n                      http:\/\/www.dcs.kcl.ac.uk\/technical-reports\/papers\/TR-08-06.pdf\n                    \n                    \n                   (updated 2010)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-30353-1_36","volume-title":"Advances in Artificial Intelligence","author":"C. Muise","year":"2012","unstructured":"Muise, C., McIlraith, S.A., Beck, J.C., Hsu, E.I.: Dsharp: Fast d-DNNF compilation with sharpSAT. In: Kosseim, L., Inkpen, D. (eds.) Canadian AI 2012. LNCS, vol.\u00a07310, pp. 356\u2013361. Springer, Heidelberg (2012)"},{"key":"16_CR21","first-page":"73","volume-title":"PLAS 2009","author":"J. Newsome","year":"2009","unstructured":"Newsome, J., McCamant, S., Song, D.: Measuring channel capacity to distinguish undue influence. In: PLAS 2009, pp. 73\u201385. ACM, New York (2009)"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Phan, Q.-S., Malacaria, P., Tkachuk, O., P\u0103s\u0103reanu, C.S.: Symbolic quantitative information flow. In: Mehlitz, P., Rungta, N., Visser, W. (eds.) Proceedings, Java Pathfinder Workshop, pp. 1\u20135 (2012)","DOI":"10.1145\/2382756.2382791"},{"key":"16_CR23","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.\u00a05504, pp. 288\u2013302. Springer, Heidelberg (2009)"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T. Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 352\u2013367. Springer, Heidelberg (2005)"},{"key":"16_CR25","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.\u00a04121, pp. 424\u2013429. Springer, Heidelberg (2006)"},{"key":"16_CR26","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-642-02716-1_24","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"C. Wernhard","year":"2009","unstructured":"Wernhard, C.: Tableaux for projection computation and knowledge compilation. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol.\u00a05607, pp. 325\u2013340. Springer, Heidelberg (2009)"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Yasuoka, H., Terauchi, T.: Quantitative information flow \u2013 verification hardness and possibilities. In: CSF 2010, pp. 15\u201327. IEEE Computer Society (2010)","DOI":"10.1109\/CSF.2010.9"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40196-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T02:56:15Z","timestamp":1557975375000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40196-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401954","9783642401961"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40196-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}