{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:36:50Z","timestamp":1725565010983},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642324949"},{"type":"electronic","value":"9783642324956"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32495-6_7","type":"book-chapter","created":{"date-parts":[[2012,7,14]],"date-time":"2012-07-14T07:54:08Z","timestamp":1342252448000},"page":"108-125","source":"Crossref","is-referenced-by-count":1,"title":["Certifying Execution Time"],"prefix":"10.1007","author":[{"given":"V\u00edtor","family":"Rodrigues","sequence":"first","affiliation":[]},{"given":"Jo\u00e3o Pedro","family":"Pedroso","sequence":"additional","affiliation":[]},{"given":"M\u00e1rio","family":"Florido","sequence":"additional","affiliation":[]},{"given":"Sim\u00e3o Melo","family":"de Sousa","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Albert, E., Arenas, P., Puebla, G., Hermenegildo, M.V.: Certificate size reduction in abstraction-carrying code. CoRR, abs\/1010.4533 (2010)"},{"issue":"1","key":"7_CR2","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.entcs.2005.01.032","volume":"132","author":"E. Albert","year":"2005","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.: An abstract interpretation-based approach to mobile code safety. Electron. Notes Theor. Comput. Sci.\u00a0132(1), 113\u2013129 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-540-75336-0_2","volume-title":"Trustworthy Global Computing","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., Beringer, L., Cr\u00e9gut, P., Gr\u00e9goire, B., Hofmann, M.O., M\u00fcller, P., Poll, E., Puebla, G., Stark, I., V\u00e9tillard, E.: MOBIUS: Mobility, Ubiquity, Security. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol.\u00a04661, pp. 10\u201329. Springer, Heidelberg (2007)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Besson, F., Cachera, D., Jensen, T., Pichardie, D.: Certified Static Analysis by Abstract Interpretation. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007\/2008\/2009. LNCS, vol.\u00a05705, pp. 223\u2013257. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-03829-7_8"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/BFb0039704","volume-title":"Formal Methods in Programming and Their Applications","author":"F. Bourdoncle","year":"1993","unstructured":"Bourdoncle, F.: Efficient Chaotic Iteration Strategies with Widenings. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol.\u00a0735, pp. 128\u2013141. Springer, Heidelberg (1993)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-642-14052-5_3","volume-title":"Interactive Theorem Proving","author":"D. Cachera","year":"2010","unstructured":"Cachera, D., Pichardie, D.: A Certified Denotational Abstract Interpreter. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 9\u201324. Springer, Heidelberg (2010)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Electronic Notes in Theoretical Computer Science\u00a06 (1997)","DOI":"10.1016\/S1571-0661(05)80168-9"},{"key":"7_CR8","series-title":"NATO ASI Series F","volume-title":"Calculational System Design","author":"P. Cousot","year":"1999","unstructured":"Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbr\u00fcggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)"},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation\u00a02, 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-45449-7_32","volume-title":"Embedded Software","author":"C. Ferdinand","year":"2001","unstructured":"Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and Precise WCET Determination for a Real-Life Processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol.\u00a02211, pp. 469\u2013485. Springer, Heidelberg (2001)"},{"key":"7_CR11","unstructured":"Hammond, K., Ferdinand, C., Heckmann, R., Dyckhoff, R., Hofmann, M., Jost, S., Loidl, H.-W., Michaelson, G., Pointon, R.F., Scaife, N., S\u00e9rot, J., Wallace, A.: Towards formally verifiable wcet analysis for a functional programming language. In: WCET (2006)"},{"key":"7_CR12","volume-title":"Introduction to operations research","author":"F.S. Hillier","year":"1986","unstructured":"Hillier, F.S., Lieberman, G.J.: Introduction to operations research, 4th edn. Holden-Day, Inc., San Francisco (1986)","edition":"4"},{"issue":"2","key":"7_CR13","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"R.M. McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Computer Science Review\u00a05(2), 119\u2013161 (2011)","journal-title":"Computer Science Review"},{"key":"7_CR14","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From system f to typed assembly language. ACM Trans. Program. Lang. Syst.\u00a021, 527\u2013568 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, pp. 106\u2013119. ACM, New York (1997)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-16442-1_10","volume-title":"ESOP 86","author":"H.R. Nielson","year":"1986","unstructured":"Nielson, H.R., Nielson, F.: Pragmatic Aspects of Two-Level Denotational Meta-Languages. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol.\u00a0213, pp. 133\u2013143. Springer, Heidelberg (1986)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Patankar, V., Jain, A., Bryant, R.: Formal verification of an arm processor. In: 12th International Conference on VLSI Design, pp. 282\u2013287 (1999)","DOI":"10.1109\/ICVD.1999.745161"},{"key":"7_CR18","unstructured":"Rodrigues, V., Florido, M., de Sousa, S.M.: Back annotation in action: from wcet analysis to source code verification. In: Actas of CoRTA 2011: Compilers, Prog. Languages, Related Technologies and Applications (July 2011)"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Rodrigues, V., Florido, M., de Sousa, S.M.: A functional approach to worst-case execution time analysis. In: 20th International Workshop on Functional and (Constraint) Logic Programming (WFLP), pp. 86\u2013103. Springer (2011)","DOI":"10.1007\/978-3-642-22531-4_6"},{"key":"7_CR20","unstructured":"Rodrigues, V., Florido, M., de Sousa, S.M.: Towards adaptive real-time systems by worst-case execution time checking. Technical report, Artificial Intelligence and Computer Science Laboratory (LIACC)- University of Porto (2011)"},{"key":"7_CR21","first-page":"189","volume-title":"Two Approaches to Interprocedural Data Flow Analysis","author":"M. Sharir","year":"1981","unstructured":"Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow Analysis, pp. 189\u2013233. Prentice-Hall, Inc., Englewood Cliffs (1981)"},{"key":"7_CR22","unstructured":"The DWARF Debugging Standard, \n                    \n                      http:\/\/www.dwarfstd.org\/"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-540-24622-0_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Wilhelm","year":"2004","unstructured":"Wilhelm, R.: Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 309\u2013322. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Foundational and Practical Aspects of Resource Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32495-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T02:10:52Z","timestamp":1556935852000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32495-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642324949","9783642324956"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32495-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}