{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T01:56:17Z","timestamp":1790819777598,"version":"4.1.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T00:00:00Z","timestamp":1436918400000},"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":["Softw Syst Model"],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1007\/s10270-015-0476-y","type":"journal-article","created":{"date-parts":[[2015,7,14]],"date-time":"2015-07-14T02:53:28Z","timestamp":1436842408000},"page":"987-1012","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["A formal verification framework for static analysis"],"prefix":"10.1007","volume":"15","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard","family":"Bubel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Germ\u00e1n","family":"Puebla","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guillermo","family":"Rom\u00e1n-D\u00edez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,7,15]]},"reference":[{"key":"476_CR1","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java bytecode. In: Proceedings of FMOODS\u201908, vol. 5051 of LNCS, pp. 2\u201318. Springer (2008)","DOI":"10.1007\/978-3-540-68863-1_2"},{"key":"476_CR2","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Field-sensitive value analysis by field-insensitive analysis. In: Proceedings of FM\u201909, vol. 5850 of LNCS, pp. 370\u2013386. Springer (2009)","DOI":"10.1007\/978-3-642-05089-3_24"},{"issue":"2","key":"476_CR3","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10817-010-9174-1","volume":"46","author":"E Albert","year":"2011","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reason. 46(2), 161\u2013203 (2011)","journal-title":"J. Autom. Reason."},{"key":"476_CR4","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.scico.2013.04.006","volume":"92","author":"E Albert","year":"2014","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Rom\u00e1n-D\u00edez, G.: Conditional termination of loops over heap-allocated data. Sci. Comput. Program. 92, 2\u201324 (2014)","journal-title":"Sci. Comput. Program."},{"key":"476_CR5","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of Java bytecode. In: European Symposium on Programming (ESOP\u201907), vol. 4421 of LNCS. Springer (2007)","DOI":"10.1007\/978-3-540-71316-6_12"},{"issue":"1","key":"476_CR6","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/j.tcs.2011.07.009","volume":"413","author":"E Albert","year":"2012","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413(1), 142\u2013159 (2012)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"476_CR7","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1017\/S1471068410000487","volume":"12","author":"E Albert","year":"2012","unstructured":"Albert, E., Arenas, P., Puebla, G., Hermenegildo, M.: Certificate size reduction in abstraction-carrying code. Theory Pract. Log. Progr. 12(3), 283\u2013318 (2012)","journal-title":"Theory Pract. Log. Progr."},{"key":"476_CR8","doi-asserted-by":"crossref","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R., Puebla, G., Rom\u00e1n-D\u00edez, G.: Verified resource guarantees using COSTA and KeY. In: Proceedings of PEPM\u201911, pp. 73\u201376 (2011)","DOI":"10.1145\/1929501.1929513"},{"key":"476_CR9","doi-asserted-by":"crossref","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R., Rom\u00e1n-D\u00edez, G.: Verified resource guarantees for heap manipulating programs. In: Proceedings of FASE\u201912, vol. 7212 of LNCS, pp. 130\u2013145. Springer, March (2012)","DOI":"10.1007\/978-3-642-28872-2_10"},{"key":"476_CR10","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., G\u00f3mez-Zamalloa, M.: Parametric inference of memory requirements for garbage collected languages. In: Proceeding of ISMM\u201910, pp. 121\u2013130. ACM Press (2010)","DOI":"10.1145\/1806651.1806671"},{"issue":"3","key":"476_CR11","doi-asserted-by":"crossref","first-page":"22:1","DOI":"10.1145\/2499937.2499943","volume":"14","author":"E Albert","year":"2013","unstructured":"Albert, E., Genaim, S., Masud, A.N.: On the inference of resource usage upper and lower bounds. ACM Trans. Comput. Log. 14(3), 22:1\u201322:35 (2013)","journal-title":"ACM Trans. Comput. Log."},{"key":"476_CR12","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Correas, J., G\u00f3mez-Zamalloa, M., Genaim, S., Puebla, G., Rom\u00e1n-D\u00edez, G.: Object-Sensitive Cost Analysis for Concurrent Objects, Technical Report. http:\/\/costa.ls.fi.upm.es\/papers\/costa\/AlbertACGGPRtr.pdf (2014)","DOI":"10.1002\/stvr.1569"},{"key":"476_CR13","doi-asserted-by":"crossref","unstructured":"Ball, T., Bounimova, E., Levin, V., Kumar, R., Lichtenberg, J.: The static driver verifier research platform. In: Proceeding of CAV\u201910, vol. 6174 of LNCS, pp. 119\u2013122. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_11"},{"key":"476_CR14","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B., DeLine, R., Jacobs, B., Rustan K., Leino, M.: Boogie: A modular reusable verifier for object-oriented programs. In: Proceedings of FMCO\u201906, vol. 4111 of LNCS, pp. 364\u2013387. Springer (2006)","DOI":"10.1007\/11804192_17"},{"key":"476_CR15","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.: Verification of object-oriented software: the KeY approach, vol. 4334 of LNCS. Springer (2006)","DOI":"10.1007\/978-3-540-69061-0"},{"key":"476_CR16","doi-asserted-by":"crossref","unstructured":"Beyer, D., Erkan Keremoglu M.: CPAchecker: A tool for configurable software verification. In: Computer Aided Verification, vol. 6806 of LNCS, pp. 184\u2013190. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"476_CR17","doi-asserted-by":"crossref","unstructured":"Blazy, S., Maroneze, A., Pichardie, D.: Formal verification of loop bound estimation for WCET analysis. In: Proceedings of VSTTE\u201913, vol. 8164 of LNCS, pp. 281\u2013303. Springer (2013)","DOI":"10.1007\/978-3-642-54108-7_15"},{"key":"476_CR18","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Computer Aided Verification, vol. 8044 of LNCS, pp. 413\u2013429. Springer, Berlin Heidelberg (2013)","DOI":"10.1007\/978-3-642-39799-8_28"},{"key":"476_CR19","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/j.entcs.2007.11.015","volume":"199","author":"R Bubel","year":"2008","unstructured":"Bubel, R., Roth, A., R\u00fcmmer, P.: Ensuring the correctness of lightweight tactics for JavaCard dynamic logic. Electron. Notes Theor. Comput. Sci. 199, 107\u2013128 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"476_CR20","doi-asserted-by":"crossref","unstructured":"Crary, K., Weirich, S.: Resource bound certification. In: Proceedings of POPL\u201900, pp. 184\u2013198. ACM (2000)","DOI":"10.1145\/325694.325716"},{"key":"476_CR21","doi-asserted-by":"crossref","unstructured":"Dios, De., Pe\u00f1a, R.: Certification of safe polynomial memory bounds. In: Proceedings of FM\u201911, LNCS, pp. 184\u2013199. Springer, June (2011)","DOI":"10.1007\/978-3-642-21437-0_16"},{"key":"476_CR22","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Proceeding of CAV\u201907, vol. 4590 of LNCS, pp. 173\u2013177. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"476_CR23","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K. K., Chilimbi, T. M.: Speed: precise and efficient static estimation of program computational complexity. In: Proceeding of POPL\u201909, pp. 127\u2013139. ACM (2009)","DOI":"10.1145\/1594834.1480898"},{"key":"476_CR24","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Proceedings of ESOP\u201910, vol. 6012 of LNCS, pp. 287\u2013306. Springer (2010)","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"476_CR25","doi-asserted-by":"crossref","unstructured":"Rustan, K., Leino, M.: Dafny: An automatic program verifier for functional correctness. In: Proceeding of LPAR\u201910, vol. 6355 of LNCS, pp. 348\u2013370. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"issue":"7","key":"476_CR26","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun ACM"},{"key":"476_CR27","volume-title":"The Java Virtual Machine Specification","author":"T Lindholm","year":"1996","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Addison-Wesley, Boston (1996)"},{"key":"476_CR28","doi-asserted-by":"crossref","unstructured":"Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) European Symposium on Programming (ESOP\u201905), vol. 3444 of LNCS, pp. 5\u201320. Springer (2005)","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"476_CR29","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Proceedings of POPL\u201997, pp. 106\u2013119. ACM Press (1997)","DOI":"10.1145\/263699.263712"},{"key":"476_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Proceeding of TACAS\u201998, vol. 1384 of LNCS, pp. 151\u2013166. Springer (1998)","DOI":"10.1007\/BFb0054170"},{"key":"476_CR31","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI\u201904), LNCS, pp. 239\u2013251. Springer (2004)","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"476_CR32","doi-asserted-by":"crossref","unstructured":"Secci, S., Spoto, F.: Pair-sharing analysis of object-oriented programs. In: Proceedings of SAS\u201905, vol. 3672 of LNCS, pp. 320\u2013335. Springer (2005)","DOI":"10.1007\/11547662_22"},{"key":"476_CR33","doi-asserted-by":"crossref","unstructured":"Smans, J., Jacobs, B., Piessens, F., Schulte, W.: An automatic verifier for Java-like programs based on dynamic frames. In: Proceeding of FASE\u201908, vol. 4961 of LNCS, pp. 261\u2013275. Springer (2008)","DOI":"10.1007\/978-3-540-78743-3_19"},{"key":"476_CR34","unstructured":"Spoto, F., Hill, P.M., Payet, E.: Path-length analysis of object-oriented programs. In: Proceeding of EAAI\u201906. http:\/\/profs.sci.univr.it\/spoto\/papers.html (2006)"},{"issue":"9","key":"476_CR35","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1145\/361002.361016","volume":"18","author":"B Wegbreit","year":"1975","unstructured":"Wegbreit, B.: Mechanical program analysis. Commun ACM 18(9), 528\u2013539 (1975)","journal-title":"Commun ACM"},{"key":"476_CR36","unstructured":"Wei\u00df, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic and predicate abstraction. Ph.D. thesis, Karlsruhe Institute of Technology (2011)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0476-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-015-0476-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0476-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0476-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,28]],"date-time":"2019-08-28T01:54:48Z","timestamp":1566957288000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-015-0476-y"}},"subtitle":["As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY"],"short-title":[],"issued":{"date-parts":[[2015,7,15]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["476"],"URL":"https:\/\/doi.org\/10.1007\/s10270-015-0476-y","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,7,15]]}}}