# Changeset 3335

Ignore:
Timestamp:
Jun 7, 2013, 12:18:21 PM (8 years ago)
Message:

rob

File:
1 edited

### Legend:

Unmodified
 r3334 \author{ %Roberto R.~M. Amadio$^{3,4}$ \and R.~M. Amadio$^{4}$ \and %Nicolas N.~Ayache$^4$ \and N.~Ayache$^{3,4}$ \and %François F.~Bobot$^4$ \and F.~Bobot$^{3,4}$ \and %Jacob J.~P. Boender$^1$ \and R.~Pollack$^2$ \and %Yann Y.~R\'egis-Gianas$^4$ \and Y.~R\'egis-Gianas$^{3,4}$ \and %Claudio C.~Sacerdoti Coen$^1$ \and \and INRIA (Team $\pi$r2 ) \and Universit\e Paris Diderot Universit\e Paris Diderot } properties of programs (time, space) at the source level, without loss of accuracy and with a small, trusted code base. The main software component developed is a formally certified complexity certifying compiler. The compiler developed is a certified compiler producing cost annotations. The compiler translates source code to object code and produces an instrumented copy of the source code. This instrumentation exposes at First the call graph of the program is computed. Then the computation of the cost of the function is performed by traversing its control flow graph. If the function f calls the function g then the function g is processed before the function f. The cost at a node is the maximum of the control flow graph. If the function $f$ calls the function $g$ then the function $g$ is processed before the function $f$. The cost at a node is the maximum of the costs of the successors. In the case of a loop with a body that has a constant cost for every step of the at the start of the loop. In the case of a loop with a body whose cost depends on the values of some free variables, a fresh logic function f is introduced to represent the cost of the variables, a fresh logic function $f$ is introduced to represent the cost of the loop in the logic assertions. This logic function takes the variant as a first parameter. The other parameters of f are the free variables of the body of the parameter. The other parameters of $f$ are the free variables of the body of the loop. An axiom is added to account the fact that the cost is accumulated at each step of the loop. The 8051/8052 microprocessor is a very simple one, with constant-cost instruction. It was chosen to separate the issue of exact propagation of the instructions. It was chosen to separate the issue of exact propagation of the cost model from the orthogonal problem of the static analysis of object code that may require approximations or dependent costs. memory in the 8051 is tiny, allowing only a minor number of nested calls. To support full recursion in order to test the CerCo tools also on recursive programs, the compiler manually manages a stack in external memory. programs, the compiler implements a stack in external memory. \end{enumerate} the labeling approach with type \& effect discipline \cite{typeffects} to handle languages with implicit memory management, and in experimenting with our tools in early development phases. Some larger use case is also necessary our tools in early development phases. Some larger case study is also necessary to evaluate the CerCo's prototype on industrial size programs. \bibitem{survey} \textbf{A Survey of Static Program Analysis Techniques} Wolfgang W\"ogerer. Technical report. Technische Universit\"at Wien 2005 \bibitem{cerco} \textbf{Certified Complexity}. R. Amadio, A. Asperti, N. Ayache, W.~W\"ogerer. Technical report. Technische Universit\"at Wien 2005 \bibitem{cerco} \textbf{Certified Complexity}. R.M. Amadio, A. Asperti, N. Ayache, B. Campbell, D. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I. Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd Programs}, N.  Ayache, R.M. Amadio, Y.Régis-Gianas, in Proc. FMICS, Springer LNCS 7437: 32-46, 2012, DOI:10.1007/978-3-642-32469-7\_3. 7437: 32-46, 2012. %, DOI:10.1007/978-3-642-32469-7\_3. \bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of R.M. Amadio, Y. Régis-Gianas. Proceedings of the Second international conference on Foundational and Practical Aspects of Resource Analysis FOPARA 2011 Springer LNCS 2011 \bibitem{compcert} \textbf{Formal verification of a realistic compiler}. Leroy, X. In Commun. ACM 52(7), 107–115 (2009) \bibitem{framac} \textbf{Frama-C user manual}. Correnson, L., Cuoq, P., Kirchner, F., Prevosto, V., Puccetti, A., Signoles, J., Yakobowski, B. in CEA-LIST, Software Safety Laboratory, Saclay, F-91191, LNCS 7177:72-89, 2012. \bibitem{compcert} \textbf{Formal verification of a realistic compiler}. X. Leroy,  In Commun. ACM 52(7), 107–115, 2009. \bibitem{framac} \textbf{Frama-C user manual}. L. Correnson, P. Cuoq, F. Kirchner, V. Prevosto, A. Puccetti, J. Signoles, B. Yakobowski. in CEA-LIST, Software Safety Laboratory, Saclay, F-91191, \url{http://frama-c.com/}. \bibitem{separation} \textbf{Intuitionistic reasoning about shared mutable data structure} John C. Reynolds. In Millennial Perspectives in Computer Science, pages 303–321, Houndsmill, Hampshire, 2000. Palgrave. structure} J.C. Reynolds. In Millennial Perspectives in Computer Science, pages 303–321, Houndsmill, Hampshire, 2000. Palgrave. \bibitem{lustre} \textbf{LUSTRE: a declarative language for real-time programming} Caspi, P. and Pilaud, D. and Halbwachs, N. and Plaice, J. A., In Proceedings of P. Caspi, D. Pilaud, N. Halbwachs, J.A. Plaice. In Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages ACM 1987. \bibitem{correctness} \textbf{On the correctness of an optimising assembler for the intel MCS-51 microprocessor}. Dominic P. Mulligan  and Claudio Sacerdoti Coen. In Proceedings of the Second D.P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second international conference on Certified Programs and Proofs, Springer-Verlag 2012. \bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable Real-Time Systems}, F.J. Cazorla, E. Qui˜nones, T. Vardanega, L. Cucu, B. Triquet, G. Systems}, F.J. Cazorla, E. Quiñones, T. Vardanega, L. Cucu, B. Triquet, G. Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions on Embedded Computing Systems, 2012. \bibitem{matita} \textbf{The Matita Interactive Theorem Prover}. Andrea Asperti, Claudio Sacerdoti Coen, Wilmer Ricciotti and Enrico Tassi. A. Asperti, C. Sacerdoti Coen, W. Ricciotti, E. Tassi. 23rd International Conference on Automated Deduction, CADE 2011. \bibitem{typeffects} \textbf{The Type and Effect Discipline}. Jean-Pierre Talpin and Pierre Jouvelot. \bibitem{typeffects} \textbf{The Type and Effect Discipline}. J.-P. Talpin, P. Jouvelot. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), Santa Cruz, California, USA, June 22-25, 1992. \bibitem{stateart} \textbf{The worst-case execution-time problem overview of methods and survey of tools.} Wilhelm R. et al., in  ACM Transactions on Embedded and survey of tools.} R. Wilhelm et al., in  ACM Transactions on Embedded Computing Systems, 7:1–53, May 2008.