{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T22:02:28Z","timestamp":1750456948432},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642541070"},{"type":"electronic","value":"9783642541087"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54108-7_15","type":"book-chapter","created":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T05:09:36Z","timestamp":1389762576000},"page":"281-303","source":"Crossref","is-referenced-by-count":11,"title":["Formal Verification of Loop Bound Estimation for WCET Analysis"],"prefix":"10.1007","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9","family":"Maroneze","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R.: al. Verified resource guarantees using COSTA and KeY. In: PEPM 2011, pp. 73\u201376. ACM (2011)","DOI":"10.1145\/1929501.1929513"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. Logical Methods in Computer Science\u00a07(2) (2011)","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"15_CR3","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.\u00a07437, pp. 32\u201346. Springer, Heidelberg (2012)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-28869-2_3","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2012","unstructured":"Barthe, G., Demange, D., Pichardie, D.: A formally verified SSA-based middle-end - Static Single Assignment meets CompCert. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol.\u00a07211, pp. 47\u201366. Springer, Heidelberg (2012)"},{"key":"15_CR5","unstructured":"Bedin Fran\u00e7a, R., Blazy, S., Favre-Felix, D., Leroy, X., et al.: Formally verified optimizing compilation in ACG-based flight control software. In: ERTS (2012)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Blackham, B., Shi, Y., Heiser, G.: Improving interrupt response time in a verifiable protected microkernel. In: Proc. of EuroSys, pp. 323\u2013336. ACM (2012)","DOI":"10.1145\/2168836.2168869"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-38856-9_18","volume-title":"Static Analysis","author":"S. Blazy","year":"2013","unstructured":"Blazy, S., Laporte, V., Maroneze, A., Pichardie, D.: Formal verification of a C value analysis based on abstract interpretation. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 324\u2013344. Springer, Heidelberg (2013)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI 2006, pp. 415\u2013426. ACM Press (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"15_CR9","unstructured":"Ermedahl, A., Sandberg, C., Gustafsson, J., Bygde, S., Lisper, B.: Loop bound analysis based on a combination of program slicing, abstract interpretation, and invariant analysis. In: Workshop on WCET Analysis (2007)"},{"key":"15_CR10","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":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-02658-4_7","volume-title":"Computer Aided Verification","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S.: SPEED: Symbolic complexity bound analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 51\u201362. Springer, Heidelberg (2009)"},{"key":"15_CR12","unstructured":"Gustafsson, J., Betts, A., Ermedahl, A., Lisper, B.: The M\u00e4lardalen WCET benchmarks: Past, present and future. In: Proc. WCET 2010, pp. 137\u2013147 (2010)"},{"key":"15_CR13","unstructured":"Gustafsson, J., Ermedahl, A.: Automatic derivation of path and loop annotations in object-oriented real-time programs. Scalable Computing: Practice and Experience\u00a01(2) (1998)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-33125-1_15","volume-title":"Static Analysis","author":"N. Halbwachs","year":"2012","unstructured":"Halbwachs, N., Henry, J.: When the decreasing sequence fails. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 198\u2013213. Springer, Heidelberg (2012)"},{"issue":"2","key":"15_CR15","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1109\/MSP.2012.41","volume":"10","author":"G. Heiser","year":"2012","unstructured":"Heiser, G., Murray, T.C., Klein, G.: It\u2019s time for trustworthy systems. IEEE Security & Privacy\u00a010(2), 67\u201370 (2012)","journal-title":"IEEE Security & Privacy"},{"issue":"7","key":"15_CR16","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. CACM\u00a052(7), 107\u2013115 (2009)","journal-title":"CACM"},{"issue":"5","key":"15_CR17","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/570886.570887","volume":"24","author":"G. Ramalingam","year":"2002","unstructured":"Ramalingam, G.: On loops, dominators, and dominance frontiers. ACM TOPLAS\u00a024(5), 455\u2013490 (2002)","journal-title":"ACM TOPLAS"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Ranganath, V.P., Amtoft, T., Banerjee, A., Hatcliff, J., et al.: A new foundation for control dependence and slicing for modern program structures. ACM TOPLAS\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275502"},{"key":"15_CR19","unstructured":"RTCA. DO-178C: Software considerations in airborne systems and equipment certification. Radio Technical Commission for Aeronautics Std. (2012)"},{"issue":"2","key":"15_CR20","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.ipl.2007.10.002","volume":"106","author":"T. Amtoft","year":"2008","unstructured":"Amtoft, T.: Slicing for modern program structures: a theory for eliminating irrelevant loops. Inf. Process. Lett.\u00a0106(2), 45\u201351 (2008)","journal-title":"Inf. Process. Lett."},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Tristan, J.-B., Leroy, X.: A simple, verified validator for software pipelining. In: Proc. of POPL, pp. 83\u201392. ACM Press (2010)","DOI":"10.1145\/1707801.1706311"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-71067-7_24","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Wasserrab","year":"2008","unstructured":"Wasserrab, D., Lochbihler, A.: Formalizing a framework for dynamic slicing of program dependence graphs in Isabelle\/HOL. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 294\u2013309. Springer, Heidelberg (2008)"},{"key":"15_CR23","doi-asserted-by":"crossref","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.: al. The worst-case execution-time problem \u2014 overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst.\u00a07, 36:1\u201336:53 (2008)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"15_CR24","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.\u00a06887, pp. 280\u2013297. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54108-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T22:25:19Z","timestamp":1558304719000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54108-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642541070","9783642541087"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54108-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}