{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:46:49Z","timestamp":1762102009414},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T00:00:00Z","timestamp":1491955200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s00236-017-0297-2","type":"journal-article","created":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T11:45:16Z","timestamp":1491997516000},"page":"729-764","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Approximate counting in SMT and value estimation for probabilistic programs"],"prefix":"10.1007","volume":"54","author":[{"given":"Dmitry","family":"Chistikov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rayna","family":"Dimitrova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,12]]},"reference":[{"key":"297_CR1","unstructured":"Allouche, D., de Givry, S., Schiex, T.: Toulbar2, an open source exact cost function network solver. Technical report, INRIA (2010)"},{"key":"297_CR2","doi-asserted-by":"crossref","unstructured":"Barvinok, A.: A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed. In: FOCS 93. ACM (1993)","DOI":"10.1109\/SFCS.1993.366830"},{"issue":"2","key":"297_CR3","doi-asserted-by":"crossref","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. 163(2), 510\u2013526 (2000)","journal-title":"Inf. Comput."},{"key":"297_CR4","unstructured":"Belle, V., Van\u00a0den Broeck, G., Passerini, A.: Hashing-based approximate probabilistic inference in hybrid domains. In: Proceedings of the 31st Conference on Uncertainty in Artificial Intelligence (UAI), Amsterdam (2015)"},{"key":"297_CR5","unstructured":"Belle, V., Passerini, A., Van den Broeck, G.: Probabilistic inference in hybrid domains by weighted model integration. In: Q.\u00a0Yang, M.\u00a0Wooldridge (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25\u201331, 2015, pp. 2770\u20132776. AAAI Press (2015). http:\/\/ijcai.org\/papers15\/Abstracts\/IJCAI15-392.html"},{"key":"297_CR6","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.\u00a015. ACM (2014)","DOI":"10.1145\/2594291.2594329"},{"key":"297_CR7","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":"297_CR8","unstructured":"Chakraborty, S., Fremont, D., Meel, K., Seshia, S., Vardi, M.: Distribution-aware sampling and weighted model counting for SAT. In: AAAI\u201914, pp. 1722\u20131730 (2014). http:\/\/www.aaai.org\/ocs\/index.php\/AAAI\/AAAI14\/paper\/view\/8364"},{"key":"297_CR9","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K., Vardi, M.: A scalable and nearly uniform generator of SAT witnesses. CAV, LNCS vol. 8044, pp. 608\u2013623 (2013)","DOI":"10.1007\/978-3-642-39799-8_40"},{"key":"297_CR10","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K., Vardi, M.: A scalable approximate model counter. In: CP: Constraint Programming, LNCS, vol. 8124, pp. 200\u2013216 (2013)","DOI":"10.1007\/978-3-642-40627-0_18"},{"key":"297_CR11","unstructured":"Chakraborty, S., Meel, K.S., Mistry, R., Vardi, M.Y.: Approximate probabilistic inference via word-level counting. In: Schuurmans, D., Wellman, M.P. (eds.) Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12\u201317, 2016, Phoenix, pp. 3218\u20133224. AAAI Press (2016)"},{"issue":"6","key":"297_CR12","doi-asserted-by":"publisher","first-page":"694","DOI":"10.1016\/j.ic.2009.06.006","volume":"208","author":"K Chatzikokolakis","year":"2010","unstructured":"Chatzikokolakis, K., Palamidessi, C.: Making random choices invisible to the scheduler. Inf. Comput. 208(6), 694\u2013715 (2010). doi: 10.1016\/j.ic.2009.06.006","journal-title":"Inf. Comput."},{"key":"297_CR13","doi-asserted-by":"crossref","unstructured":"Chistikov, D., Dimitrova, R., Majumdar, R.: Approximate counting in SMT and value estimation for probabilistic programs. In: Tools and Algorithms for the Construction and Analysis of Systems\u201421st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, April 11\u201318, 2015. pp. 320\u2013334 (2015)","DOI":"10.1007\/978-3-662-46681-0_26"},{"key":"297_CR14","doi-asserted-by":"publisher","unstructured":"Claret, G., Rajamani, S.K., Nori, A.V., Gordon, A.D., Borgstr\u00f6m, J.: Bayesian inference using data flow analysis. In: ESEC\/FSE\u201913, pp. 92\u2013102 (2013). doi: 10.1145\/2491411.2491423","DOI":"10.1145\/2491411.2491423"},{"key":"297_CR15","doi-asserted-by":"crossref","unstructured":"Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: ESOP, LNCS 7211, pp. 169\u2013193. Springer (2012)","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"297_CR16","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511811357","volume-title":"Modeling and Reasoning with Bayesian Networks","author":"A Darwiche","year":"2009","unstructured":"Darwiche, A.: Modeling and Reasoning with Bayesian Networks. Cambridge University Press, Cambridge (2009)"},{"key":"297_CR17","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS, TACAS\u201908\/ETAPS\u201908, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"297_CR18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511779398","volume-title":"Probability: Theory and Examples","author":"R Durrett","year":"2010","unstructured":"Durrett, R.: Probability: Theory and Examples, 4th edn. Cambridge University Press, Cambridge (2010)","edition":"4"},{"issue":"5","key":"297_CR19","doi-asserted-by":"crossref","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. 17(5), 967\u2013974 (1988)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"297_CR20","doi-asserted-by":"crossref","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 38(1), 1\u201317 (1991)","journal-title":"J. ACM"},{"key":"297_CR21","first-page":"334","volume":"2","author":"S Ermon","year":"2013","unstructured":"Ermon, S., Gomes, C., Sabharwal, A., Selman, B.: Taming the curse of dimensionality: discrete integration by hashing and optimization. ICML 2, 334\u2013342 (2013)","journal-title":"ICML"},{"key":"297_CR22","volume-title":"Competitive Markov Decision Processes","author":"J Filar","year":"1997","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Berlin (1997)"},{"key":"297_CR23","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":"297_CR24","doi-asserted-by":"crossref","unstructured":"Fredrikson, M., Jha, S.: Satisfiability modulo counting: a new approach for analyzing privacy properties. In: CSL-LICS, pp. 42:1\u201342:10. ACM (2014)","DOI":"10.1145\/2603088.2603097"},{"issue":"1","key":"297_CR25","doi-asserted-by":"crossref","first-page":"169","DOI":"10.2307\/2348941","volume":"43","author":"W Gilks","year":"1994","unstructured":"Gilks, W., Thomas, A., Spiegelhalter, D.: A language and program for complex Bayesian modelling. Statistician 43(1), 169\u2013177 (1994)","journal-title":"Statistician"},{"key":"297_CR26","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511804106","volume-title":"Computational Complexity: A Conceptual Perspective","author":"O Goldreich","year":"2008","unstructured":"Goldreich, O.: Computational Complexity: A Conceptual Perspective. Cambridge University Press, Cambridge (2008)"},{"key":"297_CR27","unstructured":"Gomes, C., Hoffmann, J., Sabharwal, A., Selman, B.: From sampling to model counting. In: IJCAI, pp. 2293\u20132299 (2007)"},{"key":"297_CR28","unstructured":"Gomes, C., Sabharwal, A., Selman, B.: Model counting. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 633\u2013654. IOS Press (2009)"},{"key":"297_CR29","doi-asserted-by":"crossref","unstructured":"Gordon, A., Henzinger, T., Nori, A., Rajamani, S., Samuel, S.: Probabilistic programming. In: FOSE 14, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"297_CR30","doi-asserted-by":"publisher","unstructured":"Han, C., Jiang, J.R.: When Boolean satisfiability meets Gaussian elimination in a simplex way. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification\u201424th International Conference, CAV 2012, Berkeley, CA, USA, July 7\u201313, 2012 Proceedings, Lecture Notes in Computer Science, vol. 7358, pp. 410\u2013426. Springer (2012). doi: 10.1007\/978-3-642-31424-7_31","DOI":"10.1007\/978-3-642-31424-7_31"},{"key":"297_CR31","doi-asserted-by":"crossref","unstructured":"Hur, C.K., Nori, A., Rajamani, S., Samuel, S.: Slicing probabilistic programs. In: PLDI, p.\u00a016. ACM (2014)","DOI":"10.1145\/2666356.2594303"},{"key":"297_CR32","unstructured":"Impagliazzo, R., Levin, L.A., Luby, M.: Pseudo-random generation from one-way functions (extended abstract). In: Proceedings of the 21st Annual ACM Symposium on Theory of Computing, May 14\u201317, 1989, Seattle, Washigton, USA, pp. 12\u201324 (1989)"},{"key":"297_CR33","unstructured":"Jerrum, M., Sinclair, A.: The Markov chain Monte Carlo method: an approach to approximate counting and integration. Approximation algorithms for NP-hard problems pp. 482\u2013520 (1996)"},{"key":"297_CR34","doi-asserted-by":"crossref","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 43, 169\u2013188 (1986)","journal-title":"TCS"},{"key":"297_CR35","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., McIver, A., Meinicke, L., Morgan, C.: Linear-invariant generation for probabilistic programs: automated support for proof-based methods. In: SAS, LNCS 6337, pp. 390\u2013406. Springer (2010)","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"297_CR36","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":"297_CR37","doi-asserted-by":"crossref","first-page":"284","DOI":"10.2307\/2318871","volume":"84","author":"V Klee","year":"1977","unstructured":"Klee, V.: Can the measure of $$\\cup [a_i, b_i]$$ \u222a [ a i , b i ] be computed in less than $$O(n\\log n)$$ O ( n log n ) steps? Am. Math. Mon. 84, 284\u2013285 (1977)","journal-title":"Am. Math. Mon."},{"key":"297_CR38","volume-title":"Probabilistic graphical models: principles and techniques","author":"D Koller","year":"2009","unstructured":"Koller, D., Friedman, N.: Probabilistic graphical models: principles and techniques. MIT Press, Cambridge (2009)"},{"key":"297_CR39","first-page":"328","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. JCSS 22, 328\u2013350 (1981)","journal-title":"JCSS"},{"key":"297_CR40","unstructured":"LattE tool. https:\/\/www.math.ucdavis.edu\/~latte"},{"issue":"195","key":"297_CR41","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1090\/S0025-5718-1991-1079024-2","volume":"57","author":"J Lawrence","year":"1991","unstructured":"Lawrence, J.: Polytope volume computation. Math. Comput. 57(195), 259\u2013271 (1991)","journal-title":"Math. Comput."},{"key":"297_CR42","doi-asserted-by":"publisher","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\u201914, pp. 575\u2013586 (2014). doi: 10.1145\/2642937.2643011","DOI":"10.1145\/2642937.2643011"},{"key":"297_CR43","doi-asserted-by":"crossref","unstructured":"Luu, L., Shinde, S., Saxena, P., Demsky, B.: A model counter for constraints over unbounded strings. In: PLDI, p.\u00a057. ACM (2014)","DOI":"10.1145\/2666356.2594331"},{"key":"297_CR44","doi-asserted-by":"crossref","unstructured":"Ma, F., Liu, S., Zhang, J.: Volume computation for Boolean combination of linear arithmetic constraints. In: CADE-22, LNCS 5663, pp. 453\u2013468. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_33"},{"key":"297_CR45","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Berlin (2005)"},{"key":"297_CR46","unstructured":"Minka, T., Winn, J., Guiver, J., Kannan, A.: Infer.NET 2.3 (2009)"},{"key":"297_CR47","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/j.scico.2005.02.008","volume":"58","author":"D Monniaux","year":"2005","unstructured":"Monniaux, D.: Abstract interpretation of programs as Markov decision processes. Sci. Comput. Progr. 58, 179\u2013205 (2005)","journal-title":"Sci. Comput. Progr."},{"key":"297_CR48","volume-title":"Advanced Compiler Design and Implementation","author":"S Muchnick","year":"1997","unstructured":"Muchnick, S.: Advanced Compiler Design and Implementation. Morgan-Kaufman, Burlington (1997)"},{"issue":"2","key":"297_CR49","first-page":"288","volume":"31","author":"C Papadimitriou","year":"1985","unstructured":"Papadimitriou, C.: Games against nature. JCSS 31(2), 288\u2013301 (1985)","journal-title":"JCSS"},{"key":"297_CR50","unstructured":"Monty Hall problem: http:\/\/en.wikipedia.org\/wiki\/Monty_Hall_problem"},{"key":"297_CR51","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.\u00a014. ACM (2014)","DOI":"10.1145\/2666356.2594294"},{"key":"297_CR52","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\/2491956.2462179"},{"issue":"1","key":"297_CR53","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1080\/00031305.1975.10479121","volume":"29","author":"S Selvin","year":"1975","unstructured":"Selvin, S.: A problem in probability. Am. Stat. 29(1), 67 (1975)","journal-title":"Am. Stat."},{"key":"297_CR54","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":"297_CR55","unstructured":"Soos, M.: CryptoMiniSat\u2014a SAT solver for cryptographic problems. http:\/\/www.msoos.org\/cryptominisat4\/"},{"key":"297_CR56","unstructured":"Soos, M.: Enhanced Gaussian elimination in DPLL-based SAT solvers. In: POS-10. Pragmatics of SAT, Edinburgh, UK, July 10, 2010, pp. 2\u201314 (2010). http:\/\/www.easychair.org\/publications\/?page=1319113489"},{"key":"297_CR57","doi-asserted-by":"crossref","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Theory and Applications of Satisfiability Testing\u2014SAT 2009, 12th International Conference, SAT 2009, Swansea, June 30\u2013July 3, 2009. Proceedings, pp. 244\u2013257 (2009)","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"297_CR58","doi-asserted-by":"crossref","first-page":"849","DOI":"10.1137\/0214060","volume":"14","author":"L Stockmeyer","year":"1985","unstructured":"Stockmeyer, L.: On approximation algorithms for $$\\#P$$ # P . SIAM J. Comput. 14, 849\u2013861 (1985)","journal-title":"SIAM J. Comput."},{"key":"297_CR59","unstructured":"Trevisan, L.: Computational complexity (CS\u00a0254), lecture 8 (2010). http:\/\/www.cs.stanford.edu\/~trevisan\/cs254-10\/lecture08.pdf"},{"issue":"1","key":"297_CR60","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209\u2013219 (1987)","journal-title":"J. ACM"},{"key":"297_CR61","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 9, 189\u2013201 (1979)","journal-title":"Theor. Comput. Sci."},{"key":"297_CR62","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 47, 85\u201393 (1986)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"297_CR63","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/s00224-014-9553-9","volume":"56","author":"M Zhou","year":"2014","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 Comput. Syst. 56(2), 347\u2013371 (2014). doi: 10.1007\/s00224-014-9553-9","journal-title":"Theory Comput. Syst."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-017-0297-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-017-0297-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-017-0297-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,23]],"date-time":"2023-08-23T03:21:36Z","timestamp":1692760896000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-017-0297-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,12]]},"references-count":63,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["297"],"URL":"https:\/\/doi.org\/10.1007\/s00236-017-0297-2","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,4,12]]}}}