Changeset 3335
 Timestamp:
 Jun 7, 2013, 12:18:21 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/fopara2013/fopara13.tex
r3334 r3335 47 47 \author{ 48 48 %Roberto 49 R.~M. Amadio$^{ 3,4}$ \and49 R.~M. Amadio$^{4}$ \and 50 50 %Nicolas 51 N.~Ayache$^ 4$ \and51 N.~Ayache$^{3,4}$ \and 52 52 %François 53 F.~Bobot$^ 4$ \and53 F.~Bobot$^{3,4}$ \and 54 54 %Jacob 55 55 J.~P. Boender$^1$ \and … … 69 69 R.~Pollack$^2$ \and 70 70 %Yann 71 Y.~R\'egisGianas$^ 4$ \and71 Y.~R\'egisGianas$^{3,4}$ \and 72 72 %Claudio 73 73 C.~Sacerdoti Coen$^1$ \and … … 81 81 \and INRIA (Team $\pi$r2 ) 82 82 \and 83 Universit\`e Paris Diderot 83 Universit\`e Paris Diderot 84 84 } 85 85 … … 96 96 properties of programs (time, space) at the source level, without loss of accuracy 97 97 and with a small, trusted code base. The main software component 98 developed is a formally certified complexity certifying compiler. The compiler98 developed is a certified compiler producing cost annotations. The compiler 99 99 translates source code to object code and produces an instrumented copy of the 100 100 source code. This instrumentation exposes at … … 825 825 First the call graph of the program is computed. 826 826 Then the computation of the cost of the function is performed by traversing its 827 control flow graph. If the function f calls the function g then the function g 828 is processed before the function f. The cost at a node is the maximum of the 827 control flow graph. If the function $f$ calls the function $g$ 828 then the function $g$ 829 is processed before the function $f$. The cost at a node is the maximum of the 829 830 costs of the successors. 830 831 In the case of a loop with a body that has a constant cost for every step of the … … 832 833 at the start of the loop. 833 834 In the case of a loop with a body whose cost depends on the values of some free 834 variables, a fresh logic function fis introduced to represent the cost of the835 variables, a fresh logic function $f$ is introduced to represent the cost of the 835 836 loop in the logic assertions. This logic function takes the variant as a first 836 parameter. The other parameters of fare the free variables of the body of the837 parameter. The other parameters of $f$ are the free variables of the body of the 837 838 loop. An axiom is added to account the fact that the cost is accumulated at each 838 839 step of the loop. … … 877 878 878 879 The 8051/8052 microprocessor is a very simple one, with constantcost 879 instruction . It was chosen to separate the issue of exact propagation of the880 instructions. It was chosen to separate the issue of exact propagation of the 880 881 cost model from the orthogonal problem of the static analysis of object code 881 882 that may require approximations or dependent costs. … … 919 920 memory in the 8051 is tiny, allowing only a minor number of nested calls. To 920 921 support full recursion in order to test the CerCo tools also on recursive 921 programs, the compiler manually manages a stack in external memory.922 programs, the compiler implements a stack in external memory. 922 923 \end{enumerate} 923 924 … … 1026 1027 the labeling approach with type \& effect discipline \cite{typeffects} 1027 1028 to handle languages with implicit memory management, and in experimenting with 1028 our tools in early development phases. Some larger use caseis also necessary1029 our tools in early development phases. Some larger case study is also necessary 1029 1030 to evaluate the CerCo's prototype on industrial size programs. 1030 1031 … … 1033 1034 1034 1035 \bibitem{survey} \textbf{A Survey of Static Program Analysis Techniques} 1035 W olfgangW\"ogerer. Technical report. Technische Universit\"at Wien 20051036 1037 \bibitem{cerco} \textbf{Certified Complexity}. R. Amadio, A. Asperti, N. Ayache,1036 W.~W\"ogerer. Technical report. Technische Universit\"at Wien 2005 1037 1038 \bibitem{cerco} \textbf{Certified Complexity}. R.M. Amadio, A. Asperti, N. Ayache, 1038 1039 B. Campbell, D. Mulligan, R. Pollack, Y. RegisGianas, C. Sacerdoti Coen, I. 1039 1040 Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd … … 1043 1044 Programs}, N. Ayache, R.M. Amadio, Y.RégisGianas, in Proc. FMICS, Springer 1044 1045 LNCS 1045 7437: 3246, 2012, DOI:10.1007/9783642324697\_3. 1046 7437: 3246, 2012. 1047 %, DOI:10.1007/9783642324697\_3. 1046 1048 1047 1049 \bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of … … 1049 1051 R.M. Amadio, Y. RégisGianas. Proceedings of the Second international conference 1050 1052 on Foundational and Practical Aspects of Resource Analysis FOPARA 2011 Springer 1051 LNCS 2011 1052 1053 \bibitem{compcert} \textbf{Formal verification of a realistic compiler}. Leroy, 1054 X. In Commun. ACM 52(7), 107–115 (2009) 1055 1056 \bibitem{framac} \textbf{FramaC user manual}. Correnson, L., Cuoq, P., Kirchner, 1057 F., Prevosto, V., Puccetti, A., Signoles, J., 1058 Yakobowski, B. in CEALIST, Software Safety Laboratory, Saclay, F91191, 1053 LNCS 7177:7289, 2012. 1054 1055 \bibitem{compcert} \textbf{Formal verification of a realistic compiler}. X. Leroy, In Commun. ACM 52(7), 107–115, 2009. 1056 1057 \bibitem{framac} \textbf{FramaC user manual}. L. Correnson, P. Cuoq, F. Kirchner, V. Prevosto, A. Puccetti, J. Signoles, 1058 B. Yakobowski. in CEALIST, Software Safety Laboratory, Saclay, F91191, 1059 1059 \url{http://framac.com/}. 1060 1060 … … 1065 1065 1066 1066 \bibitem{separation} \textbf{Intuitionistic reasoning about shared mutable data 1067 structure} John C. Reynolds. In Millennial Perspectives in Computer Science, 1068 pages 303–321, Houndsmill, 1069 Hampshire, 2000. Palgrave. 1067 structure} J.C. Reynolds. In Millennial Perspectives in Computer Science, 1068 pages 303–321, Houndsmill, Hampshire, 2000. Palgrave. 1070 1069 1071 1070 \bibitem{lustre} \textbf{LUSTRE: a declarative language for realtime 1072 1071 programming} 1073 Caspi, P. and Pilaud, D. and Halbwachs, N. and Plaice, J. A.,In Proceedings of1072 P. Caspi, D. Pilaud, N. Halbwachs, J.A. Plaice. In Proceedings of 1074 1073 the 14th ACM SIGACTSIGPLAN symposium on Principles of programming languages ACM 1075 1074 1987. … … 1077 1076 \bibitem{correctness} \textbf{On the correctness of an optimising assembler for 1078 1077 the intel MCS51 microprocessor}. 1079 D ominic P. Mulligan and ClaudioSacerdoti Coen. In Proceedings of the Second1078 D.P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second 1080 1079 international conference on Certified Programs and Proofs, SpringerVerlag 2012. 1081 1080 1082 1081 \bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable RealTime 1083 Systems}, F.J. Cazorla, E. Qui ˜nones, T. Vardanega, L. Cucu, B. Triquet, G.1082 Systems}, F.J. Cazorla, E. Quiñones, T. Vardanega, L. Cucu, B. Triquet, G. 1084 1083 Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions 1085 1084 on Embedded Computing Systems, 2012. … … 1092 1091 \bibitem{matita} 1093 1092 \textbf{The Matita Interactive Theorem Prover}. 1094 A ndrea Asperti, Claudio Sacerdoti Coen, Wilmer Ricciotti and EnricoTassi.1093 A. Asperti, C. Sacerdoti Coen, W. Ricciotti, E. Tassi. 1095 1094 23rd International Conference on Automated Deduction, CADE 2011. 1096 1095 1097 \bibitem{typeffects} \textbf{The Type and Effect Discipline}. J eanPierre Talpin1098 and PierreJouvelot.1096 \bibitem{typeffects} \textbf{The Type and Effect Discipline}. J.P. Talpin, 1097 P. Jouvelot. 1099 1098 In Proceedings of the Seventh Annual Symposium on Logic in Computer Science 1100 1099 (LICS '92), Santa Cruz, California, USA, June 2225, 1992. … … 1103 1102 \bibitem{stateart} \textbf{The worstcase executiontime problem overview of 1104 1103 methods 1105 and survey of tools.} Wilhelm R.et al., in ACM Transactions on Embedded1104 and survey of tools.} R. Wilhelm et al., in ACM Transactions on Embedded 1106 1105 Computing Systems, 7:1–53, May 2008. 1107 1106
Note: See TracChangeset
for help on using the changeset viewer.