{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:12:53Z","timestamp":1742958773940,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216898"},{"type":"electronic","value":"9783319216904"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_11","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T02:08:27Z","timestamp":1436926107000},"page":"178-194","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Symbolic Polytopes for Quantitative Interpolation and Verification"],"prefix":"10.1007","author":[{"given":"Klaus","family":"von Gleissenthall","sequence":"first","affiliation":[]},{"given":"Boris","family":"K\u00f6pf","sequence":"additional","affiliation":[]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-71316-6_12","volume-title":"Programming Languages and Systems","author":"E Albert","year":"2007","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of java bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 157\u2013172. Springer, Heidelberg (2007)"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Backes, M., K\u00f6pf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: IEEE S and P (2009)","DOI":"10.1109\/SP.2009.18"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Barvinok A.: A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed. In: FOCS (1993)","DOI":"10.1287\/moor.19.4.769"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Barvinok, A.: A Course in Convexity. American Mathematical Society (2002)","DOI":"10.1090\/gsm\/054"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In POPL (2014)","DOI":"10.1145\/2535838.2535860"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Computer Aided Verification","author":"TA Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified Horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869\u2013882. Springer, Heidelberg (2013)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-38856-9_8","volume-title":"Static Analysis","author":"N Bj\u00f8rner","year":"2013","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified Horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 105\u2013125. Springer, Heidelberg (2013)"},{"key":"11_CR8","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: SMT@IJCAR (2012)"},{"issue":"4","key":"11_CR9","doi-asserted-by":"crossref","first-page":"653","DOI":"10.24033\/asens.1572","volume":"21","author":"M Brion","year":"1988","unstructured":"Brion, M.: Points entiers dans les polyedres convexes. Ann. Sci. Ecole Norm. Sup. 21(4), 653\u2013663 (1988)","journal-title":"Ann. Sci. Ecole Norm. Sup."},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: PLDI (2015)","DOI":"10.1145\/2737924.2737955"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Cerny, P., Henzinger, T.A., Radhakrishna, A.: Quantitative abstraction refinement. In: POPL, ACM (2013)","DOI":"10.1145\/2429069.2429085"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Pavlogiannis, A., Velner, Y.: Quantitative interprocedural analysis. In: POPL (2015)","DOI":"10.1145\/2676726.2676968"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"11_CR14","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2001","unstructured":"Cormen, T.H., Stein, C., Rivest, R.L., Leiserson, C.E.: Introduction to Algorithms, 2nd edn. McGraw-Hill Higher Education, Boston (2001)","edition":"2"},{"issue":"4","key":"11_CR15","doi-asserted-by":"publisher","first-page":"1273","DOI":"10.1016\/j.jsc.2003.04.003","volume":"38","author":"JA Loera De","year":"2004","unstructured":"De Loera, J.A., Hemmecke, R., Tauzer, J., Yoshida, R.: Effective lattice point counting in rational convex polytopes. J. Symb. Comp. 38(4), 1273\u20131302 (2004)","journal-title":"J. Symb. Comp."},{"key":"11_CR16","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Fredrikson, M., Jha, S.: Satisfiability modulo counting: A new approach for analyzing privacy properties. In: LICS, IEEE (2014)","DOI":"10.1145\/2603088.2603097"},{"key":"11_CR18","volume-title":"Handbook of Satisfiability","author":"CP Gomes","year":"2009","unstructured":"Gomes, C.P., Sabharwal, A., Selman, B.: Model counting. In: Biere, A., Heule, M., Maaren, H.V., Walsh, T. (eds.) Handbook of Satisfiability. IOS Press, Amsterdam (2009)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: POPL. ACM (2009)","DOI":"10.1145\/1594834.1480912"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: precise and efficient static estimation of program computational complexity. In: POPL (2009)","DOI":"10.1145\/1480881.1480898"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL (2011)","DOI":"10.1145\/1926385.1926424"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: POPL (2011)","DOI":"10.1145\/1926385.1926427"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Jost, S., Hammond, K., Loidl, H.-W., Hofmann, M.: Static determination of quantitative resource usage for higher-order programs. In: POPL (2010)","DOI":"10.1145\/1706299.1706327"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","first-page":"260","volume-title":"Automated Deduction","author":"V Kuncak","year":"2005","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: boolean algebra with presburger arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 260\u2013277. Springer, Heidelberg (2005)"},{"key":"11_CR26","unstructured":"Lokuciejewski, P., Cordes, D., Falk, H., Marwedel, P.: A fast and precise static loop analysis based on abstract interpretation, program slicing and polytope models. In: CGO (2009)"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Luu, L., Shinde, S., Saxena, P., Demsky, B.: A model counter for constraints over unbounded strings. In: PLDI. ACM (2014)","DOI":"10.1145\/2594291.2594331"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Mardziel, P., Magill, S., Hicks, M., Srivatsa, M.: Dynamic enforcement of knowledge-based security policies. In: CSF. IEEE (2011)","DOI":"10.1109\/CSF.2011.15"},{"issue":"1","key":"11_CR29","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. TCS 345(1), 101\u2013121 (2005)","journal-title":"TCS"},{"issue":"5","key":"11_CR30","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/j.entcs.2009.11.015","volume":"253","author":"JA Navas","year":"2009","unstructured":"Navas, J.A., M\u00e9ndez-Lojo, M., Hermenegildo, M.V.: User-definable resource usage bounds analysis for java bytecode. Electr. Notes Theor. Comput. Sci. 253(5), 65\u201382 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-78163-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 218\u2013232. Springer, Heidelberg (2008)"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-87531-4_11","volume-title":"Computer Science Logic","author":"R Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 124\u2013138. Springer, Heidelberg (2008)"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for Horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347\u2013363. Springer, Heidelberg (2013)"},{"key":"11_CR35","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1999","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1999)"},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-642-00596-1_21","volume-title":"Foundations of Software Science and Computational Structures","author":"G Smith","year":"2009","unstructured":"Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 288\u2013302. Springer, Heidelberg (2009)"},{"key":"11_CR37","unstructured":"von Gleissenthall, K., K\u00f6pf, B., Rybalchenko, A.: Symbolic polytopes for quantitative interpolation and verification - extended version (2015). \n                      https:\/\/www7.in.tum.de\/~gleissen\/papers\/symb-polytopes.pdf"},{"key":"11_CR38","unstructured":"Verdoolaege, S.: Barvinok. \n                      http:\/\/freecode.com\/projects\/barvinok"},{"key":"11_CR39","unstructured":"Verdoolaege, S., Grosser, T.: Polyhedral extraction tool. In: IPACT (2012)"},{"issue":"1","key":"11_CR40","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s00453-006-1231-0","volume":"48","author":"S Verdoolaege","year":"2007","unstructured":"Verdoolaege, S., Seghir, R., Beyls, K., Loechner, V., Bruynooghe, M.: Counting integer points in parametric polytopes using Barvinok\u2019s rational functions. Algorithmica 48(1), 37\u201366 (2007)","journal-title":"Algorithmica"},{"key":"11_CR41","unstructured":"Wolfram, S.: Wolfram alpha, series expansion. \n                      http:\/\/www.wolframalpha.com\/examples\/SeriesExpansions.html"},{"key":"11_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-23702-7_22","volume-title":"Static Analysis","author":"F Zuleger","year":"2011","unstructured":"Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 280\u2013297. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:05:38Z","timestamp":1563825938000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}