Changeset 3335


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

rob

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3334 r3335  
    4747\author{
    4848%Roberto
    49 R.~M. Amadio$^{3,4}$ \and
     49R.~M. Amadio$^{4}$ \and
    5050%Nicolas
    51 N.~Ayache$^4$ \and
     51N.~Ayache$^{3,4}$ \and
    5252%François
    53 F.~Bobot$^4$ \and
     53F.~Bobot$^{3,4}$ \and
    5454%Jacob
    5555J.~P. Boender$^1$ \and
     
    6969R.~Pollack$^2$ \and
    7070%Yann
    71 Y.~R\'egis-Gianas$^4$ \and
     71Y.~R\'egis-Gianas$^{3,4}$ \and
    7272%Claudio
    7373C.~Sacerdoti Coen$^1$ \and
     
    8181\and INRIA (Team $\pi$r2 )
    8282\and
    83 Universit\`e Paris Diderot
     83Universit\`e Paris Diderot 
    8484}
    8585
     
    9696properties of programs (time, space) at the source level, without loss of accuracy
    9797and with a small, trusted code base. The main software component
    98 developed is a formally certified complexity certifying compiler. The compiler
     98developed is a certified compiler producing cost annotations. The compiler
    9999translates source code to object code and produces an instrumented copy of the
    100100source code. This instrumentation exposes at
     
    825825First the call graph of the program is computed.
    826826Then 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
     827control flow graph. If the function $f$ calls the function $g$
     828then the function $g$
     829is processed before the function $f$. The cost at a node is the maximum of the
    829830costs of the successors.
    830831In the case of a loop with a body that has a constant cost for every step of the
     
    832833at the start of the loop.
    833834In the case of a loop with a body whose cost depends on the values of some free
    834 variables, a fresh logic function f is introduced to represent the cost of the
     835variables, a fresh logic function $f$ is introduced to represent the cost of the
    835836loop in the logic assertions. This logic function takes the variant as a first
    836 parameter. The other parameters of f are the free variables of the body of the
     837parameter. The other parameters of $f$ are the free variables of the body of the
    837838loop. An axiom is added to account the fact that the cost is accumulated at each
    838839step of the loop.
     
    877878
    878879The 8051/8052 microprocessor is a very simple one, with constant-cost
    879 instruction. It was chosen to separate the issue of exact propagation of the
     880instructions. It was chosen to separate the issue of exact propagation of the
    880881cost model from the orthogonal problem of the static analysis of object code
    881882that may require approximations or dependent costs.
     
    919920memory in the 8051 is tiny, allowing only a minor number of nested calls. To
    920921support full recursion in order to test the CerCo tools also on recursive
    921 programs, the compiler manually manages a stack in external memory.
     922programs, the compiler implements a stack in external memory.
    922923\end{enumerate}
    923924
     
    10261027the labeling approach with type \& effect discipline \cite{typeffects}
    10271028to handle languages with implicit memory management, and in experimenting with
    1028 our tools in early development phases. Some larger use case is also necessary
     1029our tools in early development phases. Some larger case study is also necessary
    10291030to evaluate the CerCo's prototype on industrial size programs.
    10301031
     
    10331034
    10341035\bibitem{survey} \textbf{A Survey of Static Program Analysis Techniques}
    1035 Wolfgang W\"ogerer. Technical report. Technische Universit\"at Wien 2005
    1036 
    1037 \bibitem{cerco} \textbf{Certified Complexity}. R. Amadio, A. Asperti, N. Ayache,
     1036W.~W\"ogerer. Technical report. Technische Universit\"at Wien 2005
     1037
     1038\bibitem{cerco} \textbf{Certified Complexity}. R.M. Amadio, A. Asperti, N. Ayache,
    10381039B. Campbell, D. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I.
    10391040Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd
     
    10431044Programs}, N.  Ayache, R.M. Amadio, Y.Régis-Gianas, in Proc. FMICS, Springer
    10441045LNCS
    1045 7437: 32-46, 2012, DOI:10.1007/978-3-642-32469-7\_3.
     10467437: 32-46, 2012.
     1047%, DOI:10.1007/978-3-642-32469-7\_3.
    10461048
    10471049\bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of
     
    10491051R.M. Amadio, Y. Régis-Gianas. Proceedings of the Second international conference
    10501052on 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{Frama-C user manual}. Correnson, L., Cuoq, P., Kirchner,
    1057 F., Prevosto, V., Puccetti, A., Signoles, J.,
    1058 Yakobowski, B. in CEA-LIST, Software Safety Laboratory, Saclay, F-91191,
     1053LNCS 7177:72-89, 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{Frama-C user manual}. L. Correnson, P. Cuoq, F. Kirchner, V. Prevosto, A. Puccetti, J. Signoles,
     1058B. Yakobowski. in CEA-LIST, Software Safety Laboratory, Saclay, F-91191,
    10591059\url{http://frama-c.com/}.
    10601060
     
    10651065
    10661066\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.
     1067structure} J.C. Reynolds. In Millennial Perspectives in Computer Science,
     1068pages 303–321, Houndsmill, Hampshire, 2000. Palgrave.
    10701069
    10711070\bibitem{lustre} \textbf{LUSTRE: a declarative language for real-time
    10721071programming}
    1073 Caspi, P. and Pilaud, D. and Halbwachs, N. and Plaice, J. A., In Proceedings of
     1072P. Caspi, D. Pilaud, N. Halbwachs, J.A. Plaice. In Proceedings of
    10741073the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages ACM
    107510741987.
     
    10771076\bibitem{correctness} \textbf{On the correctness of an optimising assembler for
    10781077the intel MCS-51 microprocessor}.
    1079   Dominic P. Mulligan  and Claudio Sacerdoti Coen. In Proceedings of the Second
     1078  D.P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second
    10801079international conference on Certified Programs and Proofs, Springer-Verlag 2012.
    10811080
    10821081\bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable Real-Time
    1083 Systems}, F.J. Cazorla, E. Qui˜nones, T. Vardanega, L. Cucu, B. Triquet, G.
     1082Systems}, F.J. Cazorla, E. Quiñones, T. Vardanega, L. Cucu, B. Triquet, G.
    10841083Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions
    10851084on Embedded Computing Systems, 2012.
     
    10921091\bibitem{matita}
    10931092\textbf{The Matita Interactive Theorem Prover}.
    1094 Andrea Asperti, Claudio Sacerdoti Coen, Wilmer Ricciotti and Enrico Tassi.
     1093A. Asperti, C. Sacerdoti Coen, W. Ricciotti, E. Tassi.
    1095109423rd International Conference on Automated Deduction, CADE 2011.
    10961095
    1097 \bibitem{typeffects} \textbf{The Type and Effect Discipline}. Jean-Pierre Talpin
    1098 and Pierre Jouvelot.
     1096\bibitem{typeffects} \textbf{The Type and Effect Discipline}. J.-P. Talpin,
     1097 P. Jouvelot.
    10991098  In Proceedings of the Seventh Annual Symposium on Logic in Computer Science
    11001099(LICS '92), Santa Cruz, California, USA, June 22-25, 1992.
     
    11031102\bibitem{stateart} \textbf{The worst-case execution-time problem overview of
    11041103methods
    1105 and survey of tools.} Wilhelm R. et al., in  ACM Transactions on Embedded
     1104and survey of tools.} R. Wilhelm et al., in  ACM Transactions on Embedded
    11061105Computing Systems, 7:1–53, May 2008.
    11071106
Note: See TracChangeset for help on using the changeset viewer.