{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:31Z","timestamp":1763468191982,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,6,4]],"date-time":"2014-06-04T00:00:00Z","timestamp":1401840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K032011\/1"],"award-info":[{"award-number":["EP\/K032011\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,6,4]]},"DOI":"10.1145\/2590296.2590328","type":"proceedings-article","created":{"date-parts":[[2014,5,30]],"date-time":"2014-05-30T18:18:31Z","timestamp":1401473911000},"page":"283-292","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Abstract model counting"],"prefix":"10.1145","author":[{"given":"Quoc-Sang","family":"Phan","sequence":"first","affiliation":[{"name":"Queen Mary University of London, London, United Kingdom"}]},{"given":"Pasquale","family":"Malacaria","sequence":"additional","affiliation":[{"name":"Queen Mary University of London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2014,6,4]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Java PathFinder. http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/.  Java PathFinder. http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/."},{"key":"e_1_3_2_1_2_1","unstructured":"National Vulnerability Database. http:\/\/nvd.nist.gov\/.  National Vulnerability Database. http:\/\/nvd.nist.gov\/."},{"key":"e_1_3_2_1_3_1","unstructured":"QUAIL. https:\/\/project.inria.fr\/quail\/.  QUAIL. https:\/\/project.inria.fr\/quail\/."},{"key":"e_1_3_2_1_4_1","unstructured":"Soot: a Java Optimization Framework. http:\/\/www.sable.mcgill.ca\/soot\/.  Soot: a Java Optimization Framework. http:\/\/www.sable.mcgill.ca\/soot\/."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.18"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.24"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009380.1009669"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.19.4.769"},{"key":"e_1_3_2_1_9_1","unstructured":"Bayardo R. J. RelSat: A Propositional Satisfiability Solver and Model Counter. http:\/\/code.google.com\/p\/relsat\/.  Bayardo R. J. RelSat: A Propositional Satisfiability Solver and Model Counter. http:\/\/code.google.com\/p\/relsat\/."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958048"},{"key":"e_1_3_2_1_11_1","first-page":"1","article-title":"The good old davis-putnam procedure helps counting models","volume":"10","author":"Birnbaum E.","year":"1999","unstructured":"Birnbaum , E. , and Lozinskii , E. L . The good old davis-putnam procedure helps counting models . J. Artif. Int. Res. 10 , 1 ( June 1999 ), 457--477. Birnbaum, E., and Lozinskii, E. L. The good old davis-putnam procedure helps counting models. J. Artif. Int. Res. 10, 1 (June 1999), 457--477.","journal-title":"J. Artif. Int. Res."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.21"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/54235.54239"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1370628.1370629"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_1_16_1","unstructured":"Darwiche A. The c2d Compiler. http:\/\/reasoning.cs.ucla.edu\/c2d\/.  Darwiche A. The c2d Compiler. http:\/\/reasoning.cs.ucla.edu\/c2d\/."},{"key":"e_1_3_2_1_17_1","first-page":"431","volume-title":"Proceedings of the 22Nd USENIX Conference on Security (Berkeley, CA, USA, 2013), SEC'13, USENIX Association","author":"Doychev G.","unstructured":"Doychev , G. , Feld , D. , K\u00f6pf , B. , Mauborgne , L. , and Reineke , J . Cacheaudit: A tool for the static analysis of cache side channels . In Proceedings of the 22Nd USENIX Conference on Security (Berkeley, CA, USA, 2013), SEC'13, USENIX Association , pp. 431 -- 446 . Doychev, G., Feld, D., K\u00f6pf, B., Mauborgne, L., and Reineke, J. Cacheaudit: A tool for the static analysis of cache side channels. In Proceedings of the 22Nd USENIX Conference on Security (Berkeley, CA, USA, 2013), SEC'13, USENIX Association, pp. 431--446."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1920261.1920300"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_51"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40196-1_16"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_40"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190251"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375696.1375713"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375606"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166956.2166957"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1554339.1554349"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_3_2_1_29_1","volume-title":"2013 Imperial College Computing Student Workshop","volume":"35","author":"Phan Q.-S.","year":"2013","unstructured":"Phan , Q.-S. Self-composition by Symbolic Execution . In 2013 Imperial College Computing Student Workshop ( Dagstuhl, Germany , 2013 ), vol. 35 of OpenAccess Series in Informatics (OASIcs), Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, pp. 95--102. Phan, Q.-S. Self-composition by Symbolic Execution. In 2013 Imperial College Computing Student Workshop (Dagstuhl, Germany, 2013), vol. 35 of OpenAccess Series in Informatics (OASIcs), Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, pp. 95--102."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382756.2382791"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-8640.1993.tb00310.x"},{"key":"e_1_3_2_1_32_1","volume-title":"Symbolic pathfinder: integrating symbolic execution with model checking for java bytecode analysis. Automated Software Engineering","author":"Visser W.","year":"2013","unstructured":"P\\uas\\uareanu, C. S., Visser , W. , Bushnell , D. , Geldenhuys , J. , Mehlitz , P. , and Rungta , N . Symbolic pathfinder: integrating symbolic execution with model checking for java bytecode analysis. Automated Software Engineering ( 2013 ), 1--35. P\\uas\\uareanu, C. S., Visser, W., Bushnell, D., Geldenhuys, J., Mehlitz, P., and Rungta, N. Symbolic pathfinder: integrating symbolic execution with model checking for java bytecode analysis. Automated Software Engineering (2013), 1--35."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/3266641.3266673"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/2590708.2590710"}],"event":{"name":"ASIA CCS '14: 9th ACM Symposium on Information, Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Kyoto Japan","acronym":"ASIA CCS '14"},"container-title":["Proceedings of the 9th ACM symposium on Information, computer and communications security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2590296.2590328","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2590296.2590328","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:55:51Z","timestamp":1750229751000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2590296.2590328"}},"subtitle":["a novel approach for quantification of information leaks"],"short-title":[],"issued":{"date-parts":[[2014,6,4]]},"references-count":34,"alternative-id":["10.1145\/2590296.2590328","10.1145\/2590296"],"URL":"https:\/\/doi.org\/10.1145\/2590296.2590328","relation":{},"subject":[],"published":{"date-parts":[[2014,6,4]]},"assertion":[{"value":"2014-06-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}