{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:03Z","timestamp":1760202603484,"version":"3.41.0"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T00:00:00Z","timestamp":1249084800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2009,8]]},"abstract":"<jats:p>We present a method for certifying that the values computed by an imperative program will be bounded by polynomials in the program's inputs. To this end, we introduce<jats:italic>mwp<\/jats:italic>-matrices and define a semantic relation \u22a7 C :<jats:italic>M<\/jats:italic>, where C is a program and<jats:italic>M<\/jats:italic>is an<jats:italic>mwp<\/jats:italic>-matrix. It follows straightforwardly from our definitions that there exists<jats:italic>M<\/jats:italic>such that \u22a7 C :<jats:italic>M<\/jats:italic>holds iff every value computed by C is bounded by a polynomial in the inputs. Furthermore, we provide a syntactical proof calculus and define the relation \u22a2 C :<jats:italic>M<\/jats:italic>to hold iff there exists a derivation in the calculus where C :<jats:italic>M<\/jats:italic>is the bottom line. We prove that \u22a2 C :<jats:italic>M<\/jats:italic>implies \u22a7 C :<jats:italic>M<\/jats:italic>.<\/jats:p><jats:p>By means of exhaustive proof search, an algorithm can decide if there exists<jats:italic>M<\/jats:italic>such that the relation \u22a2 C :<jats:italic>M<\/jats:italic>holds, and thus, our results yield a computational method.<\/jats:p>","DOI":"10.1145\/1555746.1555752","type":"journal-article","created":{"date-parts":[[2009,8,11]],"date-time":"2009-08-11T13:29:23Z","timestamp":1249997363000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["A flow calculus of<i>mwp<\/i>-bounds for complexity analysis"],"prefix":"10.1145","volume":"10","author":[{"given":"Neil D.","family":"Jones","sequence":"first","affiliation":[{"name":"University of Copenhagen, Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Kristiansen","sequence":"additional","affiliation":[{"name":"University of Oslo, Oslo, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,8,14]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Aho A. V. Hopcroft J. H. and Ullman J. 1975. The Design and Analysis of Computer Algorithms. Studies in Logic and the Foundations of Mathematics. Addison-Wesley Publishing Co. Reading. Aho A. V. Hopcroft J. H. and Ullman J. 1975. The Design and Analysis of Computer Algorithms. Studies in Logic and the Foundations of Mathematics. Addison-Wesley Publishing Co. Reading."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201998"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2363.2366"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.02.007"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00009-9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00357-0"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003889"},{"key":"e_1_2_1_11_1","volume-title":"Rewriting Techniques and Applications. Lecture Notes in Computer Science","volume":"3091","author":"Jones N.","unstructured":"Jones , N. and Bohr , N . 2004. Termination analysis of the untyped lambda-calculus . In Rewriting Techniques and Applications. Lecture Notes in Computer Science , vol. 3091 . Springer, 1--23. Jones, N. and Bohr, N. 2004. Termination analysis of the untyped lambda-calculus. In Rewriting Techniques and Applications. Lecture Notes in Computer Science, vol. 3091. Springer, 1--23."},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Jones N. and Nielson F. 1994. Abstract interpretation: A semantics-based tool for program analysis. In Handbook of Logic in Computer Science S. Abramsky D. Gabbay and T. Maibaum Eds. vol. 4. Oxford Science Publications 527--629. Jones N. and Nielson F. 1994. Abstract interpretation: A semantics-based tool for program analysis. In Handbook of Logic in Computer Science S. Abramsky D. Gabbay and T. Maibaum Eds. vol. 4. Oxford Science Publications 527--629.","DOI":"10.1093\/oso\/9780198537809.003.0005"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-005-0191-0"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-007-9021-x"},{"key":"e_1_2_1_15_1","volume-title":"-H","author":"Kristiansen L.","year":"2003","unstructured":"Kristiansen , L. and Niggl , K . -H . 2003 . The garland measure and computational complexity of stack programs. Electronic Notes in Theoretical Computer Science , vol. 90 . Kristiansen, L. and Niggl, K.-H. 2003. The garland measure and computational complexity of stack programs. Electronic Notes in Theoretical Computer Science, vol. 90."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.016"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2003.08.010"},{"key":"e_1_2_1_18_1","first-page":"1","article-title":"Programming languages capturing complexity classes","volume":"12","author":"Kristiansen L.","year":"2005","unstructured":"Kristiansen , L. and Voda , P. 2005 . Programming languages capturing complexity classes . Nordic J. Comput. 12 , 1 -- 27 . (Special issue for NWPT'04). Kristiansen, L. and Voda, P. 2005. Programming languages capturing complexity classes. Nordic J. Comput. 12, 1--27. (Special issue for NWPT'04).","journal-title":"Nordic J. Comput."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"volume-title":"Proceedings of the International Workshop on Logic and Computational Complexity","author":"Leivant D.","key":"e_1_2_1_20_1","unstructured":"Leivant , D. 1995. Intrinsic theories and computational complexity . In Proceedings of the International Workshop on Logic and Computational Complexity , D. Leivant, Ed. Lecture Notes in Computer Science, vol. 960 . Springer , 177--194. Leivant, D. 1995. Intrinsic theories and computational complexity. In Proceedings of the International Workshop on Logic and Computational Complexity, D. Leivant, Ed. Lecture Notes in Computer Science, vol. 960. Springer, 177--194."},{"key":"e_1_2_1_21_1","unstructured":"Marion and P&amp;#233;choux. 2007. Resource control of object-oriented programs. arXiv:0706.2293v1 {cs.PL}. Marion and P&amp;#233;choux. 2007. Resource control of object-oriented programs. arXiv:0706.2293v1 {cs.PL}."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_12"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.10.011"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539704445597"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01620765"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1555746.1555752","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1555746.1555752","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:31Z","timestamp":1750253371000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1555746.1555752"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8]]},"references-count":23,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["10.1145\/1555746.1555752"],"URL":"https:\/\/doi.org\/10.1145\/1555746.1555752","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2009,8]]},"assertion":[{"value":"2006-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-08-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}