{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T16:02:21Z","timestamp":1781798541591,"version":"3.54.5"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319124650","type":"print"},{"value":"9783319124667","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12466-7_1","type":"book-chapter","created":{"date-parts":[[2014,10,22]],"date-time":"2014-10-22T04:44:58Z","timestamp":1413953098000},"page":"1-18","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Certified Complexity (CerCo)"],"prefix":"10.1007","author":[{"given":"Roberto M.","family":"Amadio","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Ayache","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Francois","family":"Bobot","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jaap P.","family":"Boender","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brian","family":"Campbell","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ilias","family":"Garnier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antoine","family":"Madet","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"James","family":"McKinna","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dominic P.","family":"Mulligan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mauro","family":"Piccolo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Randy","family":"Pollack","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yann","family":"R\u00e9gis-Gianas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ian","family":"Stark","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paolo","family":"Tranquilli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2014,10,22]]},"reference":[{"key":"1_CR1","unstructured":"AbsInt: aiT WCET analysis tools. http:\/\/www.absint.com\/ait\/"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/j.procs.2011.09.054","volume":"7","author":"R Amadio","year":"2011","unstructured":"Amadio, R., Asperti, A., Ayache, N., Campbell, B., Mulligan, D.P., Pollack, R., R\u00e9gis-Gianas, Y., Coen, C.S., Stark, I.: Certified complexity. Procedia Comput. Sci. 7, 175\u2013177 (2011). Proceedings of the 2nd European Future Technologies Conference and Exhibition 2011 (FET 11)","journal-title":"Procedia Comput. Sci."},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-32495-6_5","volume-title":"Foundational and Practical Aspects of Resource Analysis","author":"RM Amadio","year":"2012","unstructured":"Amadio, R.M., R\u00e9gis-Gianas, Y.: Certifying and reasoning on cost annotations of functional programs. In: Pe\u00f1a, R., van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2011. LNCS, vol. 7177, pp. 72\u201389. Springer, Heidelberg (2012). Extended version to appear in Higher Order and Symbolic Computation"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-22438-6_7","volume-title":"Automated Deduction \u2013 CADE-23","author":"A Asperti","year":"2011","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The matita interactive theorem prover. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 64\u201369. Springer, Heidelberg (2011)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-32469-7_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"N Ayache","year":"2012","unstructured":"Ayache, N., Amadio, R.M., R\u00e9gis-Gianas, Y.: Certifying and reasoning on cost annotations in C programs. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 32\u201346. Springer, Heidelberg (2012). http:\/\/dx.doi.org\/10.1007\/978-3-642-32469-7_3"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-34281-3_14","volume-title":"Formal Methods and Software Engineering","author":"F Bobot","year":"2012","unstructured":"Bobot, F., Filli\u00e2tre, J.-C.: Separation predicates: a taste of separation logic in first-order logic. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 167\u2013181. Springer, Heidelberg (2012). http:\/\/dx.doi.org\/10.1007\/978-3-642-34281-3_14"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: a declarative language for programming synchronous systems. In: POPL, pp. 178\u2013188. ACM Press (1987)","DOI":"10.1145\/41625.41641"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Cazorla, F., Qui\u00f1ones, E., Vardanega, T., Cucu, L., Triquet, B., Bernat, G., Berger, E., Abella, J., Wartel, F., Houston, M., Santinelli, L., Kosmidis, L., Lo, C., Maxim, D.: Proartis: probabilistically analysable real-time systems. Trans. Embed. Comput. Syst. (2012)","DOI":"10.1145\/2465787.2465796"},{"key":"1_CR9","unstructured":"The Certified Complexity (CerCo) project web site. http:\/\/cerco.cs.unibo.it"},{"key":"1_CR10","unstructured":"Correnson, L., Cuoq, P., Kirchner, F., Prevosto, V., Puccetti, A., Signoles, J., Yakobowski, B.: Frama-C user manual. CEA-LIST, Software Safety Laboratory, Saclay, F-91191. http:\/\/frama-c.com\/"},{"key":"1_CR11","first-page":"195","volume":"6","author":"K Hammond","year":"2005","unstructured":"Hammond, K., Dyckhoff, R., Ferdinand, C., Heckmann, R., Hofmann, M., Jost, S., Loidl, H.W., Michaelson, G., Pointon, R.F., Scaife, N., S\u00e9rot, J., Wallace, A.: The EmBounded project (project start paper). Trends Funct. Program. TFP 6, 195\u2013210 (2005)","journal-title":"Trends Funct. Program. TFP"},{"key":"1_CR12","unstructured":"Jessie Frama-C plugin. http:\/\/krakatoa.lri.fr\/"},{"issue":"7","key":"1_CR13","doi-asserted-by":"publisher","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":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-35308-6_7","volume-title":"Certified Programs and Proofs","author":"DP Mulligan","year":"2012","unstructured":"Mulligan, D.P., Sacerdoti Coen, C.: On the correctness of an optimising assembler for the intel MCS-51 microprocessor. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 43\u201359. Springer, Heidelberg (2012)"},{"issue":"2","key":"1_CR15","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1006\/inco.1994.1046","volume":"111","author":"JP Talpin","year":"1994","unstructured":"Talpin, J.P., Jouvelot, P.: The type and effect discipline. Inf. Comput. 111(2), 245\u2013296 (1994)","journal-title":"Inf. Comput."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Tranquilli, P.: Indexed labels for loop iteration dependent costs. In: QAPL. EPTCS, vol. 117, pp. 19\u201323 (2013)","DOI":"10.4204\/EPTCS.117.2"},{"issue":"3","key":"1_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1347375.1347389","volume":"7","author":"R Wilhelm","year":"2008","unstructured":"Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P.P., Staschulat, J., Stenstr\u00f6m, P.: The worst-case execution-time problem-overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst. 7(3), 1\u201353 (2008)","journal-title":"ACM Trans. Embedded Comput. Syst."},{"key":"1_CR18","unstructured":"W\u00f6gerer, W.: A survey of static program analysis techniques. Technical report, Technische Universit\u00e4t Wien (2005)"}],"container-title":["Lecture Notes in Computer Science","Foundational and Practical Aspects of Resource Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12466-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T14:51:12Z","timestamp":1676904672000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12466-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319124650","9783319124667"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12466-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"22 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}