{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T23:58:25Z","timestamp":1782431905304,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466803","type":"print"},{"value":"9783662466810","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_26","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T22:56:36Z","timestamp":1427756196000},"page":"320-334","source":"Crossref","is-referenced-by-count":20,"title":["Approximate Counting in SMT and Value Estimation for Probabilistic Programs"],"prefix":"10.1007","author":[{"given":"Dmitry","family":"Chistikov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rayna","family":"Dimitrova","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Barvinok, A.: A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed. In: FOCS 1993. ACM (1993)"},{"issue":"2","key":"26_CR2","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1006\/inco.2000.2885","volume":"163","author":"M. Bellare","year":"2000","unstructured":"Bellare, M., Goldreich, O., Petrank, E.: Uniform generation of NP-witnesses using an NP-oracle. Inf. Comput.\u00a0163(2), 510\u2013526 (2000)","journal-title":"Inf. Comput."},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Borges, M., Filieri, A., d\u2019Amorim, M., Pasareanu, C., Visser, W.: Compositional solution space quantification for probabilistic software analysis. In: PLDI, p. 15. ACM (2014)","DOI":"10.1145\/2594291.2594329"},{"key":"26_CR4","unstructured":"Chaganty, A., Nori, A., Rajamani, S.: Efficiently sampling probabilistic programs via program analysis. In: AISTATS. JMLR Proceedings, vol.\u00a031, pp. 153\u2013160. JMLR.org (2013)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Fremont, D., Meel, K., Seshia, S., Vardi, M.: Distribution-aware sampling and weighted model counting for SAT. In: AAAI 2014, pp. 1722\u20131730 (2014)","DOI":"10.1609\/aaai.v28i1.8990"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1007\/978-3-642-39799-8_40","volume-title":"Computer Aided Verification","author":"S. Chakraborty","year":"2013","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable and nearly uniform generator of SAT witnesses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 608\u2013623. Springer, Heidelberg (2013)"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-40627-0_18","volume-title":"Principles and Practice of Constraint Programming","author":"S. Chakraborty","year":"2013","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable approximate model counter. In: Schulte, C. (ed.) CP 2013. LNCS, vol.\u00a08124, pp. 200\u2013216. Springer, Heidelberg (2013)"},{"key":"26_CR8","unstructured":"Chistikov, D., Dimitrova, R., Majumdar, R.: Approximate counting in SMT and value estimation for probabilistic programs. CoRR, abs\/1411.0659 (2014)"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Claret, G., Rajamani, S.K., Nori, A.V., Gordon, A.D., Borgstr\u00f6m, J.: Bayesian inference using data flow analysis. In: ESEC\/FSE 2013, pp. 92\u2013102 (2013)","DOI":"10.1145\/2491411.2491423"},{"key":"26_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 De","year":"2008","unstructured":"De Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"5","key":"26_CR11","doi-asserted-by":"publisher","first-page":"967","DOI":"10.1137\/0217060","volume":"17","author":"M. Dyer","year":"1988","unstructured":"Dyer, M., Frieze, A.: On the complexity of computing the volume of a polyhedron. SIAM J. Comput.\u00a017(5), 967\u2013974 (1988)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"26_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/102782.102783","volume":"38","author":"M. Dyer","year":"1991","unstructured":"Dyer, M., Frieze, A., Kannan, R.: A random polynomial time algorithm for approximating the volume of convex bodies. J. ACM\u00a038(1), 1\u201317 (1991)","journal-title":"J. ACM"},{"key":"26_CR13","unstructured":"Ermon, S., Gomes, C., Sabharwal, A., Selman, B.: Taming the curse of dimensionality: Discrete integration by hashing and optimization. In: ICML (2), pp. 334\u2013342 (2013)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Filieri, A., Pasareanu, C., Visser, W.: Reliability analysis in symbolic Pathfinder. In: ICSE, pp. 622\u2013631 (2013)","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Fredrikson, M., Jha, S.: Satisfiability modulo counting: A new approach for analyzing privacy properties. In: CSL-LICS, p. 42. ACM (2014)","DOI":"10.1145\/2603088.2603097"},{"key":"26_CR16","unstructured":"Gomes, C., Hoffmann, J., Sabharwal, A., Selman, B.: From sampling to model counting. In: IJCAI, pp. 2293\u20132299 (2007)"},{"key":"26_CR17","unstructured":"Gomes, C., Sabharwal, A., Selman, B.: Model counting. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 633\u2013654. IOS Press (2009)"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Gordon, A., Henzinger, T., Nori, A., Rajamani, S., Samuel, S.: Probabilistic programming. In: FOSE 2014, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Hur, C.-K., Nori, A., Rajamani, S., Samuel, S.: Slicing probabilistic programs. In: PLDI, p. 16. ACM (2014)","DOI":"10.1145\/2594291.2594303"},{"key":"26_CR20","unstructured":"Jerrum, M., Sinclair, A.: The Markov chain Monte Carlo method: An approach to approximate counting and integration. In: Approximation Algorithms for NP-hard Problems, pp. 482\u2013520. PWS Publishing (1996)"},{"key":"26_CR21","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(86)90174-X","volume":"43","author":"M. Jerrum","year":"1986","unstructured":"Jerrum, M., Valiant, L., Vazirani, V.: Random generation of combinatorial structures from a uniform distribution. TCS\u00a043, 169\u2013188 (1986)","journal-title":"TCS"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Kiselyov, O., Shan, C.-C.: Monolingual probabilistic programming using generalized coroutines. In: UAI, pp. 285\u2013292. AUAI Press (2009)","DOI":"10.1007\/978-3-642-03034-5_17"},{"key":"26_CR23","unstructured":"LattE tool, https:\/\/www.math.ucdavis.edu\/~latte"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"Luckow, K.S., Pasareanu, C.S., Dwyer, M.B., Filieri, A., Visser, W.: Exact and approximate probabilistic symbolic execution for nondeterministic programs. In: ASE 2014, pp. 575\u2013586 (2014)","DOI":"10.1145\/2642937.2643011"},{"key":"26_CR25","doi-asserted-by":"crossref","unstructured":"Luu, L., Shinde, S., Saxena, P., Demsky, B.: A model counter for constraints over unbounded strings. In: PLDI, p. 57. ACM (2014)","DOI":"10.1145\/2594291.2594331"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Ma, F., Liu, S., Zhang, J.: Volume computation for boolean combination of linear arithmetic constraints. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 453\u2013468. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_33"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Sampson, A., Panchekha, P., Mytkowicz, T., McKinley, K., Grossman, D., Ceze, L.: Expressing and verifying probabilistic assertions. In: PLDI, p. 14. ACM Press (2014)","DOI":"10.1145\/2594291.2594294"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: PLDI, pp. 447\u2013458. ACM (2013)","DOI":"10.1145\/2499370.2462179"},{"issue":"1","key":"26_CR29","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1080\/00031305.1975.10479121","volume":"29","author":"S. Selvin","year":"1975","unstructured":"Selvin, S.: A problem in probability. American Statistician\u00a029(1), 67 (1975)","journal-title":"American Statistician"},{"key":"26_CR30","doi-asserted-by":"crossref","unstructured":"Sipser, M.: A complexity-theoretic approach to randomness. In: STOC, pp. 330\u2013335. ACM (1983)","DOI":"10.1145\/800061.808762"},{"key":"26_CR31","doi-asserted-by":"publisher","first-page":"849","DOI":"10.1137\/0214060","volume":"14","author":"L. Stockmeyer","year":"1985","unstructured":"Stockmeyer, L.: On approximation algorithms for #P. SIAM J. of Computing\u00a014, 849\u2013861 (1985)","journal-title":"SIAM J. of Computing"},{"issue":"1","key":"26_CR32","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM\u00a034(1), 209\u2013219 (1987)","journal-title":"J. ACM"},{"key":"26_CR33","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0304-3975(79)90044-6","volume":"9","author":"L. Valiant","year":"1979","unstructured":"Valiant, L.: The complexity of computing the permanent. Theoretical Computer Science\u00a09, 189\u2013201 (1979)","journal-title":"Theoretical Computer Science"},{"key":"26_CR34","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0304-3975(86)90135-0","volume":"47","author":"L. Valiant","year":"1986","unstructured":"Valiant, L., Vazirani, V.: NP is as easy as detecting unique solutions. Theoretical Computer Science\u00a047, 85\u201393 (1986)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"26_CR35","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/s00224-014-9553-9","volume":"56","author":"M. Zhou","year":"2015","unstructured":"Zhou, M., He, F., Song, X., He, S., Chen, G., Gu, M.: Estimating the volume of solution space for satisfiability modulo linear real arithmetic. Theory of Computing Systems\u00a056(2), 347\u2013371 (2015)","journal-title":"Theory of Computing Systems"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,9]],"date-time":"2023-08-09T02:47:32Z","timestamp":1691549252000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}