E. Albert, R. Bubel, S. Genaim, and R. Hähnle, Verified resource guarantees using COSTA and KeY, Proceedings of the 20th ACM SIGPLAN workshop on Partial evaluation and program manipulation, PERM '11, pp.73-76, 2011.
DOI : 10.1145/1929501.1929513
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.186.2576

R. Atkey, Amortised resource analysis with separation logic, Logical Methods in Computer Science, vol.7, issue.2, 2011.

N. Ayache, R. M. Amadio, and Y. Régis-gianas, Certifying and Reasoning on Cost Annotations in C Programs, Proc. of FMICS, pp.32-46, 2012.
DOI : 10.1007/978-3-642-32469-7_3
URL : https://hal.archives-ouvertes.fr/hal-00702665

G. Barthe, D. Demange, and D. Pichardie, A formally verified SSA-based middleend -Static Single Assignment meets CompCert, Proc. of ESOP, pp.47-66, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01110783

R. Bedin-frança, S. Blazy, D. Favre-felix, and X. Leroy, Formally verified optimizing compilation in ACG-based flight control software, ERTS, 2012.

B. Blackham, Y. Shi, and G. Heiser, Improving interrupt response time in a verifiable protected microkernel, Proceedings of the 7th ACM european conference on Computer Systems, EuroSys '12, pp.323-336, 2012.
DOI : 10.1145/2168836.2168869

S. Blazy, V. Laporte, A. Maroneze, and D. Pichardie, Formal Verification of a C Value Analysis Based on Abstract Interpretation, Proc. of Static Analysis Symposium (SAS), 2013.
DOI : 10.1007/978-3-642-38856-9_18
URL : https://hal.archives-ouvertes.fr/hal-00812515

B. Cook, A. Podelski, and A. Rybalchenko, Termination proofs for systems code, PLDI 2006, pp.415-426, 2006.
DOI : 10.1145/1133255.1134029
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.166.164

A. Ermedahl, C. Sandberg, J. Gustafsson, S. Bygde, and B. Lisper, Loop bound analysis based on a combination of program slicing, abstract interpretation, and invariant analysis, Workshop on WCET Analysis, 2007.

F. Bourdoncle, Efficient chaotic iteration strategies with widenings, Proc. of FMPA 1993, pp.128-141, 1993.
DOI : 10.1007/BFb0039704

S. Gulwani, SPEED: Symbolic Complexity Bound Analysis, Proc. of CAV, pp.51-62, 2009.
DOI : 10.1007/978-3-642-02658-4_7

J. Gustafsson, A. Betts, A. Ermedahl, and B. Lisper, The Mälardalen WCET benchmarks: Past, present and future, Proc. WCET 2010, pp.137-147, 2010.

J. Gustafsson and A. Ermedahl, Automatic derivation of path and loop annotations in object-oriented real-time programs. Scalable Computing: Practice and Experience, 1998.

N. Halbwachs and J. Henry, When the Decreasing Sequence Fails, Proc. of Static Analysis Symposium (SAS), pp.198-213, 2012.
DOI : 10.1007/978-3-642-33125-1_15
URL : https://hal.archives-ouvertes.fr/hal-00734340

G. Heiser, T. C. Murray, and G. Klein, It's Time for Trustworthy Systems, IEEE Security & Privacy Magazine, vol.10, issue.2, pp.67-70, 2012.
DOI : 10.1109/MSP.2012.41

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

G. Ramalingam, On loops, dominators, and dominance frontiers, ACM Transactions on Programming Languages and Systems, vol.24, issue.5, pp.455-490, 2002.
DOI : 10.1145/570886.570887

V. P. Ranganath, T. Amtoft, A. Banerjee, and J. Hatcliff, A new foundation for control dependence and slicing for modern program structures, ACM Transactions on Programming Languages and Systems, vol.29, issue.5, p.29, 2007.
DOI : 10.1145/1275497.1275502

R. Do-178c, Software considerations in airborne systems and equipment certification. Radio Technical Commission for Aeronautics Std, 2012.

T. Amtoft, Slicing for modern program structures: a theory for eliminating irrelevant loops, Information Processing Letters, vol.106, issue.2, pp.45-51, 2008.
DOI : 10.1016/j.ipl.2007.10.002

J. Tristan and X. Leroy, A simple, verified validator for software pipelining, Proc. of POPL, pp.83-92, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00529836

D. Wasserrab and A. Lochbihler, Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL, Proc. of TPHOL, pp.294-309, 2008.
DOI : 10.1145/1216374.1216375

R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, and S. Thesing, The worst-case execution-time problem???overview of methods and survey of tools, ACM Transactions on Embedded Computing Systems, vol.7, issue.3, pp.1-36, 2008.
DOI : 10.1145/1347375.1347389

F. Zuleger, S. Gulwani, M. Sinn, and H. Veith, Bound Analysis of Imperative Programs with the Size-Change Abstraction, Proc. of Static Analysis Symposium (SAS), pp.280-297, 2011.
DOI : 10.1007/978-3-642-19835-9_9