- Timestamp:
- May 28, 2014, 11:01:39 AM (7 years ago)
- Location:
- Papers/fopara2013
- Files:
-
- 1 added
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.bib
r3462 r3469 34 34 title={Certifying and Reasoning on Cost Annotations in {C} Programs}, 35 35 url={http://dx.doi.org/10.1007/978-3-642-32469-7_3}, 36 author={Ayache, Nicolas and Amadio, RobertoM. and R\'egis-Gianas, Yann}, 37 pages={32--46} 36 author={Ayache, Nicolas and Amadio, Roberto and R\'egis-Gianas, Yann}, 37 pages={32--46}, 38 publisher={Springer Berlin Heidelberg} 38 39 } 39 40 … … 45 46 doi={10.1007/978-3-642-32495-6_5}, 46 47 title={Certifying and Reasoning on Cost Annotations of Functional Programs}, 47 author={Amadio, Roberto M.and R\'egis-Gianas, Yann},48 author={Amadio, Roberto and R\'egis-Gianas, Yann}, 48 49 pages={72--89}, 49 note={Extended version to appear in Higher Order and Symbolic Computation, 2013} 50 note={Extended version to appear in Higher Order and Symbolic Computation}, 51 publisher={Springer Berlin Heidelberg} 50 52 } 51 53 -
Papers/fopara2013/fopara13.tex
r3462 r3469 1118 1118 to evaluate the CerCo's prototype on realistic, industrial-scale programs. 1119 1119 1120 \begin{thebibliography}{10} 1121 \providecommand{\url}[1]{\texttt{#1}} 1122 \providecommand{\urlprefix}{URL } 1123 1124 \bibitem{absint} 1125 {AbsInt}: {aiT WCET} analysis tools, \url{http://www.absint.com/ait/} 1126 1127 \bibitem{cerco} 1128 Amadio, 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) 1132 1133 \bibitem{labelling2} 1134 Amadio, 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 1138 1139 \bibitem{matita} 1140 Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: The {Matita} interactive 1141 theorem prover. In: CADE. LNCS, vol. 6803, pp. 64--69. Springer (2011) 1142 1143 \bibitem{labelling} 1144 Ayache, 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{http://dx.doi.org/10.1007/978-3-642-32469-7_3} 1148 1149 \bibitem{bobot} 1150 Bobot, 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{http://dx.doi.org/10.1007/978-3-642-34281-3_14} 1154 1155 \bibitem{lustre} 1156 Caspi, 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) 1159 1160 \bibitem{proartis} 1161 Cazorla, 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) 1165 1166 \bibitem{cerco-website} 1167 The {Certified Complexity} ({CerCo}) project web site, 1168 \url{http://cerco.cs.unibo.it} 1169 1170 \bibitem{framac} 1171 Correnson, 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{http://frama-c.com/} 1174 1175 \bibitem{embounded} 1176 Hammond, 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) 1180 1181 \bibitem{jessie} 1182 Jessie {Frama-C} plugin, \url{http://krakatoa.lri.fr/} 1183 1184 \bibitem{compcert} 1185 Leroy, X.: Formal verification of a realistic compiler. Communications of the 1186 ACM 52(7), 107--115 (2009) 1187 1188 \bibitem{correctness} 1189 Mulligan, 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) 1191 1192 \bibitem{typeffects} 1193 Talpin, J.P., Jouvelot, P.: The type and effect discipline. Inf. Comput. 1194 111(2), 245--296 (1994) 1195 1196 \bibitem{paolo} 1197 Tranquilli, P.: Indexed labels for loop iteration dependent costs. In: QAPL. 1198 EPTCS, vol. 117, pp. 19--23 (2013) 1199 1200 \bibitem{stateart} 1201 Wilhelm, 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) 1206 1207 \bibitem{survey} 1208 W\"ogerer, W.: A survey of static program analysis techniques. Tech. rep., 1209 Technische Universit\"at Wien (2005) 1210 1211 \end{thebibliography} 1212 1120 1213 % \bibliographystyle{splncs} 1121 \bibliography{fopara13}1214 %\bibliography{fopara13} 1122 1215 % \begin{thebibliography}{19} 1123 1216 % … … 1203 1296 %\bibliography{fopara13.bib} 1204 1297 1205 \appendix1206 1207 \include{appendix}1208 1209 1298 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.