Changeset 3469 for Papers

Timestamp:

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

Author:

mulligan

Message:

added final zip file commited to easychair

Location:

Papers/fopara2013

Files:

• fopara13.bib (modified) (2 diffs)
• fopara13.tex (modified) (2 diffs)
• fopara13.zip (added)

Papers/fopara2013/fopara13.bib

@@ -34 +34 @@
 title={Certifying and Reasoning on Cost Annotations in {C} Programs},
 url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
-author={Ayache, Nicolas and Amadio, RobertoM. and R\'egis-Gianas, Yann},
-pages={32--46}
+author={Ayache, Nicolas and Amadio, Roberto and R\'egis-Gianas, Yann},
+pages={32--46},
+publisher={Springer Berlin Heidelberg}
 }
 
@@ -45 +46 @@
 doi={10.1007/978-3-642-32495-6_5},
 title={Certifying and Reasoning on Cost Annotations of Functional Programs},
-author={Amadio, RobertoM. and R\'egis-Gianas, Yann},
+author={Amadio, Roberto and R\'egis-Gianas, Yann},
 pages={72--89},
-note={Extended version to appear in Higher Order and Symbolic Computation, 2013}
+note={Extended version to appear in Higher Order and Symbolic Computation},
+publisher={Springer Berlin Heidelberg}
 }
 

Papers/fopara2013/fopara13.tex

@@ -1118 +1118 @@
 to evaluate the CerCo's prototype on realistic, industrial-scale programs.
 
+\begin{thebibliography}{10}
+\providecommand{\url}[1]{\texttt{#1}}
+\providecommand{\urlprefix}{URL }
+
+\bibitem{absint}
+{AbsInt}: {aiT WCET} analysis tools, \url{http://www.absint.com/ait/}
+
+\bibitem{cerco}
+Amadio, R., Asperti, A., Ayache, N., Campbell, B., Mulligan, D.P., Pollack, R.,
+  R{\'e}gis-Gianas, Y., Coen, C.S., Stark, I.: Certified complexity. Procedia
+  Computer Science  7,  175--177 (2011), proceedings of the 2nd European Future
+  Technologies Conference and Exhibition 2011 (FET 11)
+
+\bibitem{labelling2}
+Amadio, R., R\'egis-Gianas, Y.: Certifying and reasoning on cost annotations of
+  functional programs. In: Foundational and Practical Aspects of Resource
+  Analysis, LNCS, vol. 7177, pp. 72--89. Springer Berlin Heidelberg (2012),
+  extended version to appear in Higher Order and Symbolic Computation
+
+\bibitem{matita}
+Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: The {Matita} interactive
+  theorem prover. In: CADE. LNCS, vol. 6803, pp. 64--69. Springer (2011)
+
+\bibitem{labelling}
+Ayache, N., Amadio, R., R\'egis-Gianas, Y.: Certifying and reasoning on cost
+  annotations in {C} programs. In: Formal Methods for Industrial Critical
+  Systems, LNCS, vol. 7437, pp. 32--46. Springer Berlin Heidelberg (2012),
+  \url{http://dx.doi.org/10.1007/978-3-642-32469-7_3}
+
+\bibitem{bobot}
+Bobot, F., Filliâtre, J.C.: Separation predicates: A taste of separation logic
+  in first-order logic. In: Formal Methods and Software Engineering. Lecture
+  Notes in Computer Science, vol. 7635, pp. 167--181 (2012),
+  \url{http://dx.doi.org/10.1007/978-3-642-34281-3_14}
+
+\bibitem{lustre}
+Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: A declarative
+  language for programming synchronous systems. In: POPL. pp. 178--188. ACM
+  Press (1987)
+
+\bibitem{proartis}
+Cazorla, F., Qui{\~n}ones, 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. Transactions on Embedded Computing Systems  (2012)
+
+\bibitem{cerco-website}
+The {Certified Complexity} ({CerCo}) project web site,
+  \url{http://cerco.cs.unibo.it}
+
+\bibitem{framac}
+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, \url{http://frama-c.com/}
+
+\bibitem{embounded}
+Hammond, K., Dyckhoff, R., Ferdinand, C., Heckmann, R., Hofmann, M., Jost, S.,
+  Loidl, H.W., Michaelson, G., Pointon, R.F., Scaife, N., S{\'e}rot, J.,
+  Wallace, A.: {The {EmBounded} Project (Project Start Paper)}. In: TFP. Trends
+  in Functional Programming, vol.~6, pp. 195--210 (2005)
+
+\bibitem{jessie}
+Jessie {Frama-C} plugin, \url{http://krakatoa.lri.fr/}
+
+\bibitem{compcert}
+Leroy, X.: Formal verification of a realistic compiler. Communications of the
+  ACM  52(7),  107--115 (2009)
+
+\bibitem{correctness}
+Mulligan, D.P., Sacerdoti~Coen, C.: On the correctness of an optimising
+  assembler for the {Intel MCS-51} microprocessor. In: CPP. pp. 43--59 (2012)
+
+\bibitem{typeffects}
+Talpin, J.P., Jouvelot, P.: The type and effect discipline. Inf. Comput.
+  111(2),  245--296 (1994)
+
+\bibitem{paolo}
+Tranquilli, P.: Indexed labels for loop iteration dependent costs. In: QAPL.
+  EPTCS, vol. 117, pp. 19--23 (2013)
+
+\bibitem{stateart}
+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{\"o}m, P.: The worst-case
+  execution-time problem---overview of methods and survey of tools. ACM Trans.
+  Embedded Comput. Syst.  7(3) (2008)
+
+\bibitem{survey}
+W\"ogerer, W.: A survey of static program analysis techniques. Tech. rep.,
+  Technische Universit\"at Wien (2005)
+
+\end{thebibliography}
+
 % \bibliographystyle{splncs}
-\bibliography{fopara13}
+%\bibliography{fopara13}
 % \begin{thebibliography}{19}
 % 
@@ -1203 +1296 @@
 %\bibliography{fopara13.bib}
 
-\appendix
-
-\include{appendix}
-
 \end{document}