{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T07:06:37Z","timestamp":1765609597071},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,6,13]],"date-time":"2014-06-13T00:00:00Z","timestamp":1402617600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s00224-014-9553-9","type":"journal-article","created":{"date-parts":[[2014,6,12]],"date-time":"2014-06-12T06:59:39Z","timestamp":1402556379000},"page":"347-371","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic"],"prefix":"10.1007","volume":"56","author":[{"given":"Min","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fei","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoyu","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shi","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gangyi","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ming","family":"Gu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,6,13]]},"reference":[{"issue":"6","key":"9553_CR1","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"100","author":"SB Akers","year":"1978","unstructured":"Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. 100(6), 509\u2013516 (1978)","journal-title":"IEEE Trans. Comput."},{"issue":"4","key":"9553_CR2","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/s12045-008-0014-0","volume":"13","author":"K Athreya","year":"2008","unstructured":"Athreya, K.: Unit ball in high dimensions. Resonance 13(4), 334\u2013342 (2008)","journal-title":"Resonance"},{"issue":"2","key":"9553_CR3","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1080\/10556789808805706","volume":"10","author":"D Avis","year":"1998","unstructured":"Avis, D.: Computational experience with the reverse search vertex enumeration algorithm. Optim. Methods Softw. 10(2), 107\u2013124 (1998)","journal-title":"Optim. Methods Softw."},{"key":"9553_CR4","doi-asserted-by":"crossref","unstructured":"Avis, D.: A revised implementation of the reverse search vertex enumeration algorithm. In: Polytopescombinatorics and Computation, pp. 177\u2013198. Springer (2000)","DOI":"10.1007\/978-3-0348-8438-9_9"},{"key":"9553_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Larus, J.R.: Branch prediction for free. In: Proceedings of PLDI\u201993, pp. 300\u2013313. ACM, New York (1993)","DOI":"10.1145\/173262.155119"},{"key":"9553_CR6","first-page":"825","volume":"185","author":"C Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. Handb. Satisfiability 185, 825\u2013885 (2009)","journal-title":"Handb. Satisfiability"},{"key":"9553_CR7","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Computer Aided Verification, pp. 298\u2013302. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"9553_CR8","doi-asserted-by":"crossref","unstructured":"B\u00fceler, B., Enge, A., Fukuda, K.: Exact volume computation for polytopes: a practical study. In: Polytopes-Combinatorics and Computation, pp. 131\u2013154. Springer (2000)","DOI":"10.1007\/978-3-0348-8438-9_6"},{"key":"9553_CR9","doi-asserted-by":"crossref","unstructured":"Buse, R. P., Weimer, W.: The road not taken: estimating path execution frequency statically. In: Proceedings of ICSE\u201909, pp. 144\u2013154. IEEE Computer Society (2009)","DOI":"10.1109\/ICSE.2009.5070516"},{"key":"9553_CR10","unstructured":"Dantzig, G. B.: Linear Programming and Extensions. Princeton university press (1998)"},{"key":"9553_CR11","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9553_CR12","doi-asserted-by":"crossref","unstructured":"Dutertre, B., De Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Proceedings of CAV\u201906, pp. 81\u201394. Springer (2006)","DOI":"10.1007\/11817963_11"},{"key":"9553_CR13","unstructured":"Dutertre, B., De Moura, L.: The yices SMT solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf , 2, 2, (2006)"},{"issue":"1","key":"9553_CR14","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. JACM 38(1), 1\u201317 (1991)","journal-title":"JACM"},{"issue":"5","key":"9553_CR15","doi-asserted-by":"crossref","first-page":"967","DOI":"10.1137\/0217060","volume":"17","author":"ME Dyer","year":"1988","unstructured":"Dyer, M.E., Frieze, A.M.: On the complexity of computing the volume of a polyhedron. SIAM J. Comput. 17(5), 967\u2013974 (1988)","journal-title":"SIAM J. Comput."},{"key":"9553_CR16","unstructured":"Gr\u00f6tschel, M., Lov\u00e1sz, L., Schrijver, A.: Geometric Algorithms and Combinatorial Optimization. Springer (1988). http:\/\/eudml.org\/doc\/204187"},{"key":"9553_CR17","doi-asserted-by":"crossref","unstructured":"Huang, J., Darwiche, A.: Using DPLL for efficient OBDD construction. In: Theory and Applications of Satisfiability Testing, pp. 157\u2013172. Springer (2005)","DOI":"10.1007\/11527695_13"},{"issue":"1","key":"9553_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1002\/(SICI)1098-2418(199708)11:1<1::AID-RSA1>3.0.CO;2-X","volume":"11","author":"R Kannan","year":"1997","unstructured":"Kannan, R., Lov\u00e1sz, L., Simonovits, M.: Random walks and an O \u2217(n 5) volume algorithm for convex bodies. Random Struct. Algoritm. 11(1), 1\u201350 (1997)","journal-title":"Random Struct. Algoritm."},{"issue":"7","key":"9553_CR19","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":"9553_CR20","doi-asserted-by":"crossref","unstructured":"Liu, S., Zhang, J.: Program analysis: from qualitative analysis to quantitative analysis (nier track). In: Proceedings of ICSE\u201911, pp. 956\u2013959. IEEE (2011)","DOI":"10.1145\/1985793.1985957"},{"key":"9553_CR21","doi-asserted-by":"crossref","unstructured":"Liu, S., Zhang, J., Zhu, B.: Volume computation using a direct monte carlo method. In: Computing and Combinatorics, pp. 198\u2013209. Springer (2007)","DOI":"10.1007\/978-3-540-73545-8_21"},{"issue":"4","key":"9553_CR22","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1002\/rsa.3240040402","volume":"4","author":"L Lov\u00e1sz","year":"1993","unstructured":"Lov\u00e1sz, L., Simonovits, M.: Random walks in a convex body and an improved volume algorithm. Random Struct. Algoritm. 4(4), 359\u2013412 (1993)","journal-title":"Random Struct. Algoritm."},{"issue":"2","key":"9553_CR23","doi-asserted-by":"crossref","first-page":"392","DOI":"10.1016\/j.jcss.2005.08.004","volume":"72","author":"L Lov\u00e1sz","year":"2006","unstructured":"Lov\u00e1sz, L., Vempala, S.: Simulated annealing in convex bodies and an O \u2217(n 4) volume algorithm. J. Comput. Syst. Sci. 72(2), 392\u2013417 (2006)","journal-title":"J. Comput. Syst. Sci."},{"key":"9553_CR24","doi-asserted-by":"crossref","unstructured":"Ma, F., Liu, S., Zhang, J.: Volume computation for boolean combination of linear arithmetic constraints. In: Proceedings of CADE\u201909, pp. 453\u2013468. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_33"},{"issue":"2","key":"9553_CR25","doi-asserted-by":"crossref","first-page":"645","DOI":"10.1214\/aoms\/1177692644","volume":"43","author":"G Marsaglia","year":"1972","unstructured":"Marsaglia, G.: Choosing a point from the surface of a sphere. Ann. Math. Stat. 43(2), 645\u2013646 (1972)","journal-title":"Ann. Math. Stat."},{"key":"9553_CR26","doi-asserted-by":"crossref","unstructured":"Necula, G. C.: Proof-Carrying Code. Design and Implementation. Springer (2002)","DOI":"10.1007\/978-94-010-0413-8_8"},{"key":"9553_CR27","unstructured":"Nelson, C. G.: Techniques for program verification. XEROX Research Center (1981)"},{"issue":"6","key":"9553_CR28","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). JACM 53(6), 937\u2013977 (2006)","journal-title":"JACM"},{"issue":"4","key":"9553_CR29","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"CS P\u0103s\u0103reanu","year":"2009","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Softw. Tools Technol. Transfer 11(4), 339\u2013353 (2009)","journal-title":"Softw. Tools Technol. Transfer"},{"issue":"6","key":"9553_CR30","doi-asserted-by":"crossref","first-page":"763","DOI":"10.1109\/TSE.2010.24","volume":"36","author":"S Poulding","year":"2010","unstructured":"Poulding, S., Clark, J.A.: Efficient software verification: Statistical testing using automated search. IEEE Trans. Softw. Eng. 36(6), 763\u2013777 (2010)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"9553_CR31","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/BF02591902","volume":"27","author":"S Smale","year":"1983","unstructured":"Smale, S.: On the average number of steps of the simplex method of linear programming. Math. Program. 27(3), 241\u2013262 (1983)","journal-title":"Math. Program."},{"key":"9553_CR32","doi-asserted-by":"crossref","unstructured":"Wei, W., Selman, B.: A new approach to model counting. In: Theory and Applications of Satisfiability Testing, pp. 324\u2013339. Springer (2005)","DOI":"10.1007\/11499107_24"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-014-9553-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-014-9553-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-014-9553-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,11]],"date-time":"2019-08-11T13:07:38Z","timestamp":1565528858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-014-9553-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,13]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["9553"],"URL":"https:\/\/doi.org\/10.1007\/s00224-014-9553-9","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,6,13]]}}}