{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T12:15:04Z","timestamp":1725884104234},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319572871"},{"type":"electronic","value":"9783319572888"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57288-8_9","type":"book-chapter","created":{"date-parts":[[2017,4,8]],"date-time":"2017-04-08T06:45:05Z","timestamp":1491633905000},"page":"131-138","source":"Crossref","is-referenced-by-count":12,"title":["Model-Counting Approaches for Nonlinear Numerical Constraints"],"prefix":"10.1007","author":[{"given":"Mateus","family":"Borges","sequence":"first","affiliation":[]},{"given":"Quoc-Sang","family":"Phan","sequence":"additional","affiliation":[]},{"given":"Antonio","family":"Filieri","sequence":"additional","affiliation":[]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,4,9]]},"reference":[{"key":"9_CR1","unstructured":"ISSTAC: Integrated Symbolic Execution for Space-Time Analysis of Code. http:\/\/www.cmu.edu\/silicon-valley\/research\/isstac"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Backes, M., Kopf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: SP 2009, pp. 141\u2013153 (2009)","DOI":"10.1109\/SP.2009.18"},{"key":"9_CR3","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: FSE 2016, pp. 193\u2013204. ACM (2016)","DOI":"10.1145\/2950290.2950362"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Borges, M., Filieri, A., d\u2019Amorim, M., P\u0103s\u0103reanu, C.S., Visser, W.: Compositional solution space quantification for probabilistic software analysis. In: PLDI, pp. 123\u2013132. ACM (2014)","DOI":"10.1145\/2666356.2594329"},{"issue":"9","key":"9_CR5","doi-asserted-by":"crossref","first-page":"1326","DOI":"10.1016\/j.jsc.2008.02.017","volume":"44","author":"M Brickenstein","year":"2009","unstructured":"Brickenstein, M., Dreyer, A.: PolyBoRi: a framework for gr\u00f6bner-basis computations with boolean polynomials. J. Symb. Comput. 44(9), 1326\u20131345 (2009)","journal-title":"J. Symb. Comput."},{"key":"9_CR6","unstructured":"Brumley, D., Boneh, D.: Remote timing attacks are practical. In: SSYM 2003, pp. 1\u20131. USENIX Association (2003)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Mistry, R., Vardi, M.Y.: Approximate probabilistic inference via word-level counting. In: AAAI 2016, pp. 3218\u20133224 (2016)","DOI":"10.1609\/aaai.v30i1.10416"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-662-46681-0_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Chistikov","year":"2015","unstructured":"Chistikov, D., Dimitrova, R., Majumdar, R.: Approximate counting in SMT and value estimation for probabilistic programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 320\u2013334. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_26"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_7"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Filieri, A., P\u0103s\u0103reanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: ICSE, pp. 622\u2013631. IEEE Press (2013)","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"9_CR12","unstructured":"Gao, S.: Counting zeros over finite fields using Gr\u00f6bner bases. Master\u2019s thesis, Carnegie Mellon University (2009)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-30494-4_20","volume-title":"Formal Methods in Computer-Aided Design","author":"O Grumberg","year":"2004","unstructured":"Grumberg, O., Schuster, A., Yadgar, A.: Memory efficient all-solutions SAT solver and its application for reachability analysis. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 275\u2013289. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30494-4_20"},{"issue":"7","key":"9_CR14","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-40196-1_16","volume-title":"Quantitative Evaluation of Systems","author":"V Klebanov","year":"2013","unstructured":"Klebanov, V., Manthey, N., Muise, C.: SAT-based analysis and quantification of information flow in programs. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 177\u2013192. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40196-1_16"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Klebanov, V., Weigl, A., Weisbarth, J.: Sound probabilistic #SAT with projection. In: QAPL 2016, pp. 15\u201329 (2016)","DOI":"10.4204\/EPTCS.227.2"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/3-540-68697-5_9","volume-title":"Advances in Cryptology \u2014 CRYPTO 1996","author":"PC Kocher","year":"1996","unstructured":"Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 104\u2013113. Springer, Heidelberg (1996). doi: 10.1007\/3-540-68697-5_9"},{"issue":"4","key":"9_CR18","doi-asserted-by":"crossref","first-page":"1273","DOI":"10.1016\/j.jsc.2003.04.003","volume":"38","author":"JAD Loera","year":"2004","unstructured":"Loera, J.A.D., Hemmecke, R., Tauzer, J., Yoshida, R.: Effective lattice point counting in rational convex polytopes. J. Symb. Comput. 38(4), 1273\u20131302 (2004)","journal-title":"J. Symb. Comput."},{"key":"9_CR19","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1017\/S0960129513000649","volume":"25","author":"P Malacaria","year":"2015","unstructured":"Malacaria, P.: Algebraic foundations for quantitative information flow. Math. Struct. Comput. Sci. 25, 404\u2013428 (2015)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9_CR20","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":"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.) AI 2012. LNCS (LNAI), vol. 7310, pp. 356\u2013361. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-30353-1_36"},{"key":"9_CR21","unstructured":"Phan, Q.S.: Model counting modulo theories. Ph.D. thesis, Queen Mary University of London (2015)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Phan, Q.S., Malacaria, P.: All-solution satisfiability modulo theories: applications, algorithms and benchmarks. In: ARES 2015, pp. 100\u2013109 (2015)","DOI":"10.1109\/ARES.2015.14"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Phan, Q.S., Malacaria, P., P\u0103s\u0103reanu, C.S., d\u2019Amorim, M.: Quantifying information leaks using reliability analysis. In: SPIN 2014, pp. 105\u2013108. ACM (2014)","DOI":"10.1145\/2632362.2632367"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C.S., Phan, Q.S., Malacaria, P.: Multi-run side-channel analysis using Symbolic Execution and Max-SMT. In: CSF 2016, pp. 387\u2013400, June 2016","DOI":"10.1109\/CSF.2016.34"},{"key":"9_CR25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10515-013-0122-2","volume":"20","author":"CS P\u0103s\u0103reanu","year":"2013","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W., Bushnell, D., Geldenhuys, J., Mehlitz, P., Rungta, N.: Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Autom. Softw. Eng. 20, 1\u201335 (2013)","journal-title":"Autom. Softw. Eng."},{"issue":"2","key":"9_CR26","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/s11009-011-9242-y","volume":"15","author":"R Rubinstein","year":"2013","unstructured":"Rubinstein, R.: Stochastic enumeration method for counting NP-hard problems. Methodol. Comput. Appl. Probab. 15(2), 249\u2013291 (2013)","journal-title":"Methodol. Comput. Appl. Probab."},{"key":"9_CR27","unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 3.0.0 (2015)"},{"key":"9_CR28","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). doi: 10.1007\/11814948_38"},{"key":"9_CR29","unstructured":"Tran, Q., Vardi, M.Y.: Groebner bases computation in boolean rings for symbolic model checking. In: MOAS, pp. 440\u2013445. ACTA Press (2007)"},{"key":"9_CR30","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning: 2: Classical Papers on Computational Logic","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning: 2: Classical Papers on Computational Logic, pp. 466\u2013483. Springer, Heidelberg (1983)"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/11499107_24","volume-title":"Theory and Applications of Satisfiability Testing","author":"W Wei","year":"2005","unstructured":"Wei, W., Selman, B.: A new approach to model counting. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 324\u2013339. Springer, Heidelberg (2005). doi: 10.1007\/11499107_24"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57288-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,23]],"date-time":"2023-08-23T02:03:59Z","timestamp":1692756239000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57288-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319572871","9783319572888"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57288-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}