Changeset 3469

May 28, 2014, 11:01:39 AM (7 years ago)

added final zip file commited to easychair

1 added
2 edited


  • Papers/fopara2013/fopara13.bib

    r3462 r3469  
    3434title={Certifying and Reasoning on Cost Annotations in {C} Programs},
    36 author={Ayache, Nicolas and Amadio, RobertoM. and R\'egis-Gianas, Yann},
    37 pages={32--46}
     36author={Ayache, Nicolas and Amadio, Roberto and R\'egis-Gianas, Yann},
     38publisher={Springer Berlin Heidelberg}
    4647title={Certifying and Reasoning on Cost Annotations of Functional Programs},
    47 author={Amadio, RobertoM. and R\'egis-Gianas, Yann},
     48author={Amadio, Roberto and R\'egis-Gianas, Yann},
    49 note={Extended version to appear in Higher Order and Symbolic Computation, 2013}
     50note={Extended version to appear in Higher Order and Symbolic Computation},
     51publisher={Springer Berlin Heidelberg}
  • Papers/fopara2013/fopara13.tex

    r3462 r3469  
    11181118to evaluate the CerCo's prototype on realistic, industrial-scale programs.
     1122\providecommand{\urlprefix}{URL }
     1125{AbsInt}: {aiT WCET} analysis tools, \url{}
     1128Amadio, R., Asperti, A., Ayache, N., Campbell, B., Mulligan, D.P., Pollack, R.,
     1129  R{\'e}gis-Gianas, Y., Coen, C.S., Stark, I.: Certified complexity. Procedia
     1130  Computer Science  7,  175--177 (2011), proceedings of the 2nd European Future
     1131  Technologies Conference and Exhibition 2011 (FET 11)
     1134Amadio, R., R\'egis-Gianas, Y.: Certifying and reasoning on cost annotations of
     1135  functional programs. In: Foundational and Practical Aspects of Resource
     1136  Analysis, LNCS, vol. 7177, pp. 72--89. Springer Berlin Heidelberg (2012),
     1137  extended version to appear in Higher Order and Symbolic Computation
     1140Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: The {Matita} interactive
     1141  theorem prover. In: CADE. LNCS, vol. 6803, pp. 64--69. Springer (2011)
     1144Ayache, N., Amadio, R., R\'egis-Gianas, Y.: Certifying and reasoning on cost
     1145  annotations in {C} programs. In: Formal Methods for Industrial Critical
     1146  Systems, LNCS, vol. 7437, pp. 32--46. Springer Berlin Heidelberg (2012),
     1147  \url{}
     1150Bobot, F., Filliâtre, J.C.: Separation predicates: A taste of separation logic
     1151  in first-order logic. In: Formal Methods and Software Engineering. Lecture
     1152  Notes in Computer Science, vol. 7635, pp. 167--181 (2012),
     1153  \url{}
     1156Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: A declarative
     1157  language for programming synchronous systems. In: POPL. pp. 178--188. ACM
     1158  Press (1987)
     1161Cazorla, F., Qui{\~n}ones, E., Vardanega, T., Cucu, L., Triquet, B., Bernat,
     1162  G., Berger, E., Abella, J., Wartel, F., Houston, M., Santinelli, L.,
     1163  Kosmidis, L., Lo, C., Maxim, D.: Proartis: Probabilistically analysable
     1164  real-time systems. Transactions on Embedded Computing Systems  (2012)
     1167The {Certified Complexity} ({CerCo}) project web site,
     1168  \url{}
     1171Correnson, L., Cuoq, P., Kirchner, F., Prevosto, V., Puccetti, A., Signoles,
     1172  J., Yakobowski, B.: Frama-{C} user manual. CEA-LIST, Software Safety
     1173  Laboratory, Saclay, F-91191, \url{}
     1176Hammond, K., Dyckhoff, R., Ferdinand, C., Heckmann, R., Hofmann, M., Jost, S.,
     1177  Loidl, H.W., Michaelson, G., Pointon, R.F., Scaife, N., S{\'e}rot, J.,
     1178  Wallace, A.: {The {EmBounded} Project (Project Start Paper)}. In: TFP. Trends
     1179  in Functional Programming, vol.~6, pp. 195--210 (2005)
     1182Jessie {Frama-C} plugin, \url{}
     1185Leroy, X.: Formal verification of a realistic compiler. Communications of the
     1186  ACM  52(7),  107--115 (2009)
     1189Mulligan, D.P., Sacerdoti~Coen, C.: On the correctness of an optimising
     1190  assembler for the {Intel MCS-51} microprocessor. In: CPP. pp. 43--59 (2012)
     1193Talpin, J.P., Jouvelot, P.: The type and effect discipline. Inf. Comput.
     1194  111(2),  245--296 (1994)
     1197Tranquilli, P.: Indexed labels for loop iteration dependent costs. In: QAPL.
     1198  EPTCS, vol. 117, pp. 19--23 (2013)
     1201Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B.,
     1202  Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I.,
     1203  Puschner, P.P., Staschulat, J., Stenstr{\"o}m, P.: The worst-case
     1204  execution-time problem---overview of methods and survey of tools. ACM Trans.
     1205  Embedded Comput. Syst.  7(3) (2008)
     1208W\"ogerer, W.: A survey of static program analysis techniques. Tech. rep.,
     1209  Technische Universit\"at Wien (2005)
    11201213% \bibliographystyle{splncs}
    1121 \bibliography{fopara13}
    11221215% \begin{thebibliography}{19}
    1205 \appendix
    1207 \include{appendix}
Note: See TracChangeset for help on using the changeset viewer.