Ignore:
Timestamp:
Jun 7, 2013, 6:02:21 PM (7 years ago)
Author:
tranquil
Message:

passed biblio to bibtex, and some aesthetical changes

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Papers/fopara2013/fopara13.tex

    r3337 r3339  
    110110\section{Introduction}
    111111
    112 \paragraph{Problem statement} Computer programs can be specified with both
     112\paragraph{Problem statement.} Computer programs can be specified with both
    113113functional constraints (what a program must do) and non-functional constraints
    114114(e.g. what resources---time, space, etc.---the program may use).  In the current
    … …  
    130130the estimates.
    131131
    132 \paragraph{Vision and approach} We want to reconcile functional and
     132\paragraph{Vision and approach.} We want to reconcile functional and
    133133non-functional analyses: to share information and perform both at the same time
    134134on source code.
    … …  
    155155components.
    156156
    157 \paragraph{Contributions} We have developed what we refer to as \emph{the labeling approach} \cite{labeling}, a
     157\paragraph{Contributions.} We have developed what we refer to as \emph{the labeling approach} \cite{labeling}, a
    158158technique to implement compilers that induce cost models on source programs by
    159159very lightweight tracking of code changes through compilation. We have studied
    … …  
    449449\begin{lstlisting}
    450450|int __cost = 33; int __stack = 5, __stack_max = 5;|
    451 
    452451|void __cost_incr(int incr) { __cost = __cost + incr; }|
    453 
    454452|void __stack_incr(int incr) {
    455453  __stack = __stack + incr;
    … …  
    478476  /*@ for time_cost: loop invariant
    479477        __cost <=
    480         \at(__cost,__l)+220*(__max(\at(5-j,__l), 0)-__max (5-j, 0));
     478        \at(__cost,__l)+220*(__max(\at(5-j,__l), 0)
     479                       -__max (5-j, 0));
    481480      for stack_cost: loop invariant
    482481        __stack_max == \at(__stack_max,__l);
    … …  
    509508\label{itest1}
    510509\end{figure}
    511 \section{Main S\&T results of the CerCo project}
    512 We will now review the main S\&T results achieved in the CerCo project.
     510\section{Main scientific and technical results}
     511We will now review the main results that the CerCo project has achieved.
    513512
    514513% \emph{Dependent labeling~\cite{?}.} The basic labeling approach assumes a
    … …  
    569568bounded by a program-dependent constant (precision property).
    570569
    571 \paragraph{The labeling software components} We solve the problem in four
     570\paragraph{The labeling software components.} We solve the problem in four
    572571stages \cite{labeling}, implemented by four software components that are used
    573572in sequence.
    … …  
    615614The obtained source code is the instrumented source code.
    616615
    617 \paragraph{Correctness} Requirements 1, 2 and 3 of the problem statement
     616\paragraph{Correctness.} Requirements 1, 2 and 3 of the problem statement
    618617obviously hold, with 2 and 3 being a consequence of the definition of a correct
    619618labeling preserving compiler. It is also obvious that the value of the global
    … …  
    765764a proof automatically, otherwise, user interaction is required.
    766765
    767 \paragraph{The Cost plugin and its application to the Lustre compiler}
     766\paragraph{The Cost plugin and its application to the Lustre compiler.}
    768767Frama-C \cite{framac} is a set of analysers for C programs with a
    769768specification language called ACSL. New analyses can be dynamically added
    … …  
    784783Lustre compiler.
    785784
    786 \paragraph{Soundness} The soundness of the whole framework depends on the cost
     785\paragraph{Soundness.} The soundness of the whole framework depends on the cost
    787786annotations added by the CerCo compiler, the synthetic costs produced by the
    788787cost plugin, the verification conditions (VCs) generated by Jessie, and the
    … …  
    799798composed of branching and assignments (no loops and no recursion) because a fine
    800799analysis of the VCs associated with branching may lead to a complexity blow up.
    801 \paragraph{Experience with Lustre} Lustre is a data-flow language for programming
     800\paragraph{Experience with Lustre.} Lustre is a data-flow language for programming
    802801synchronous systems, with the language coming with a compiler to C. We designed a
    803802wrapper for supporting Lustre files.
    … …  
    809808Ergo is able to discharge all VCs automatically.
    810809
    811 \paragraph{Handling C programs with simple loops}
     810\paragraph{Handling C programs with simple loops.}
    812811The cost annotations added by the CerCo compiler take the form of C instructions
    813812that update by a constant a fresh global variable called the cost variable.
    … …  
    8448432) by annotating functions with cost specifications. The plugin will use this cost
    845844for the function instead of computing it.
    846 \paragraph{C programs with pointers}
     845\paragraph{C programs with pointers.}
    847846When it comes to verifying programs involving pointer-based data structures,
    848847such as linked lists, trees, or graphs, the use of traditional first-order logic
    … …  
    897896Ecole Polytechnique.
    898897
    899 The main peculiarities of the CerCo compiler are:
     898The main peculiarities of the CerCo compiler are the following.
    900899\begin{enumerate}
    901 \item all of our intermediate languages include label emitting instructions to
    902 implement the labeling approach, and the compiler preserves execution traces,
    903 \item traditionally compilers target an assembly language with additional
     900\item All the intermediate languages include label emitting instructions to
     901implement the labeling approach, and the compiler preserves execution traces.
     902\item Traditionally compilers target an assembly language with additional
    904903macro-instructions to be expanded before assembly; for CerCo we need to go all
    905904the way down to object code in order to perform the static analysis. Therefore
    906 we integrated also an optimising assembler and a static analyser,
    907 \item to avoid implementing a linker and a loader, we do not support separate
    908 compilation and external calls. Adding a linker and a loader is a transparent
    909 process to the labeling approach and should create no unknown problem,
    910 \item we target an 8-bit processor. Targeting an 8-bit processor requires
     905we integrated also an optimising assembler and a static analyser.
     906\item In order to avoid implementing a linker and a loader, we do not support separate
     907compilation and external calls. Adding them is a transparent
     908process to the labeling approach and should create no unknown problem.
     909\item We target an 8-bit processor. Targeting an 8-bit processor requires
    911910several changes and increased code size, but it is not fundamentally more
    912 complex. The proof of correctness, however, becomes much harder,
    913 \item we target a microprocessor that has a non uniform memory model, which is
     911complex. The proof of correctness, however, becomes much harder.
     912\item We target a microprocessor that has a non uniform memory model, which is
    914913still often the case for microprocessors used in embedded systems and that is
    915914becoming common again in multi-core processors. Therefore the compiler has to
    916915keep track of data and it must move data between memory regions in the proper
    917 way. Also the size of pointers to different regions is not uniform. An
     916way. Moreover the size of pointers to different regions is not uniform. An
    918917additional difficulty was that the space available for the stack in internal
    919918memory in the 8051 is tiny, allowing only a minor number of nested calls. To
    … …  
    947946out to be more complex than what we expected at the beginning.
    948947
    949 \paragraph{The statement}
     948\paragraph{The statement.}
    950949Real time programs are often reactive programs that loop forever responding to
    951950events (inputs) by performing some computation followed by some action (output)
    … …  
    10281027to evaluate the CerCo's prototype on realistic, industrial-scale programs.
    10291028
    1030 \bibliographystyle{llncs}
    1031 \begin{thebibliography}{19}
    1032 
    1033 \bibitem{survey} \textbf{A Survey of Static Program Analysis Techniques}
    1034 W.~W\"ogerer. Technical report. Technische Universit\"at Wien 2005
    1035 
    1036 \bibitem{cerco} \textbf{Certified Complexity}. R.M. Amadio, A. Asperti, N. Ayache,
    1037 B. Campbell, D. P. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I.
    1038 Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd
    1039 European Future Technologies Conference and Exhibition 2011 (FET 11), 175-177.
    1040 
    1041 \bibitem{labeling} \textbf{Certifying and Reasoning on Cost Annotations in C
    1042 Programs}, N.  Ayache, R.M. Amadio, Y.R\'{e}gis-Gianas, in Proc. FMICS, Springer
    1043 LNCS
    1044 7437: 32-46, 2012.
    1045 %, DOI:10.1007/978-3-642-32469-7\_3.
    1046 
    1047 \bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of
    1048 functional programs}.
    1049 R.M. Amadio, Y. R\'{e}gis-Gianas. Proceedings of the Second international conference
    1050 on Foundational and Practical Aspects of Resource Analysis FOPARA 2011 Springer
    1051 LNCS 7177:72-89, 2012.
    1052 
    1053 \bibitem{compcert} \textbf{Formal verification of a realistic compiler}. X. Leroy,  In Commun. ACM 52(7), 107–115, 2009.
    1054 
    1055 \bibitem{framac} \textbf{Frama-C user manual}. L. Correnson, P. Cuoq, F. Kirchner, V. Prevosto, A. Puccetti, J. Signoles,
    1056 B. Yakobowski. in CEA-LIST, Software Safety Laboratory, Saclay, F-91191,
    1057 \url{http://frama-c.com/}.
    1058 
    1059 \bibitem{paolo} \textbf{Indexed Labels for Loop Iteration Dependent Costs}. P.
    1060 Tranquilli, in Proceedings of the 11th International Workshop on Quantitative
    1061 Aspects of Programming Languages and Systems (QAPL 2013), Rome, 23rd-24th March
    1062 2013, Electronic Proceedings in Theoretical Computer Science, to appear in 2013.
    1063 
    1064 \bibitem{separation} \textbf{Intuitionistic reasoning about shared mutable data
    1065 structure} J.C. Reynolds. In Millennial Perspectives in Computer Science,
    1066 pages 303–321, Houndsmill, Hampshire, 2000. Palgrave.
    1067 
    1068 \bibitem{lustre} \textbf{LUSTRE: a declarative language for real-time
    1069 programming}
    1070 P. Caspi, D. Pilaud, N. Halbwachs, J.A. Plaice. In Proceedings of
    1071 the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages ACM
    1072 1987.
    1073 
    1074 \bibitem{correctness} \textbf{On the correctness of an optimising assembler for
    1075 the intel MCS-51 microprocessor}.
    1076   D. P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second
    1077 international conference on Certified Programs and Proofs, Springer-Verlag 2012.
    1078 
    1079 \bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable Real-Time
    1080 Systems}, F.J. Cazorla, E. Qui\~{n}ones, T. Vardanega, L. Cucu, B. Triquet, G.
    1081 Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions
    1082 on Embedded Computing Systems, 2012.
    1083 
    1084 \bibitem{embounded} \textbf{The EmBounded project (project paper)}. K. Hammond,
    1085 R. Dyckhoff, C. Ferdinand, R. Heckmann, M. Hofmann, H. Loidl, G. Michaelson, J.
    1086 Serot, A. Wallace, in Trends in Functional Programming, Volume 6, Intellect
    1087 Press, 2006.
    1088 
    1089 \bibitem{matita}
    1090 \textbf{The Matita Interactive Theorem Prover}.
    1091 A. Asperti, C. Sacerdoti Coen, W. Ricciotti, E. Tassi.
    1092 23rd International Conference on Automated Deduction, CADE 2011.
    1093 
    1094 \bibitem{typeffects} \textbf{The Type and Effect Discipline}. J.-P. Talpin,
    1095  P. Jouvelot.
    1096   In Proceedings of the Seventh Annual Symposium on Logic in Computer Science
    1097 (LICS '92), Santa Cruz, California, USA, June 22-25, 1992.
    1098 IEEE Computer Society 1992.
    1099 
    1100 \bibitem{stateart} \textbf{The worst-case execution-time problem overview of
    1101 methods
    1102 and survey of tools.} R. Wilhelm et al., in  ACM Transactions on Embedded
    1103 Computing Systems, 7:1–53, May 2008.
    1104 
    1105 %\bibitem{proartis2} \textbf{A Cache Design for Probabilistic Real-Time
    1106 % Systems}, L. Kosmidis, J. Abella, E. Quinones, and F. Cazorla, in Design,
    1107 % Automation, and Test in Europe (DATE), Grenoble, France, 03/2013.
    1108 
    1109 \end{thebibliography}
     1029% \bibliographystyle{splncs}
     1030\bibliography{fopara13}
     1031% \begin{thebibliography}{19}
     1032%
     1033% \bibitem{survey} \textbf{A Survey of Static Program Analysis Techniques}
     1034% W.~W\"ogerer. Technical report. Technische Universit\"at Wien 2005
     1035%
     1036% \bibitem{cerco} \textbf{Certified Complexity}. R.M. Amadio, A. Asperti, N. Ayache,
     1037% B. Campbell, D. P. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I.
     1038% Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd
     1039% European Future Technologies Conference and Exhibition 2011 (FET 11), 175-177.
     1040%
     1041% \bibitem{labeling} \textbf{Certifying and Reasoning on Cost Annotations in C
     1042% Programs}, N.  Ayache, R.M. Amadio, Y.R\'{e}gis-Gianas, in Proc. FMICS, Springer
     1043% LNCS
     1044% 7437: 32-46, 2012.
     1045% %, DOI:10.1007/978-3-642-32469-7\_3.
     1046%
     1047% \bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of
     1048% functional programs}.
     1049% R.M. Amadio, Y. R\'{e}gis-Gianas. Proceedings of the Second international conference
     1050% on Foundational and Practical Aspects of Resource Analysis FOPARA 2011 Springer
     1051% LNCS 7177:72-89, 2012.
     1052%
     1053% \bibitem{compcert} \textbf{Formal verification of a realistic compiler}. X. Leroy,  In Commun. ACM 52(7), 107–115, 2009.
     1054%
     1055% \bibitem{framac} \textbf{Frama-C user manual}. L. Correnson, P. Cuoq, F. Kirchner, V. Prevosto, A. Puccetti, J. Signoles,
     1056% B. Yakobowski. in CEA-LIST, Software Safety Laboratory, Saclay, F-91191,
     1057% \url{http://frama-c.com/}.
     1058%
     1059% \bibitem{paolo} \textbf{Indexed Labels for Loop Iteration Dependent Costs}. P.
     1060% Tranquilli, in Proceedings of the 11th International Workshop on Quantitative
     1061% Aspects of Programming Languages and Systems (QAPL 2013), Rome, 23rd-24th March
     1062% 2013, Electronic Proceedings in Theoretical Computer Science, to appear in 2013.
     1063%
     1064% \bibitem{separation} \textbf{Intuitionistic reasoning about shared mutable data
     1065% structure} J.C. Reynolds. In Millennial Perspectives in Computer Science,
     1066% pages 303–321, Houndsmill, Hampshire, 2000. Palgrave.
     1067%
     1068% \bibitem{lustre} \textbf{LUSTRE: a declarative language for real-time
     1069% programming}
     1070% P. Caspi, D. Pilaud, N. Halbwachs, J.A. Plaice. In Proceedings of
     1071% the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages ACM
     1072% 1987.
     1073%
     1074% \bibitem{correctness} \textbf{On the correctness of an optimising assembler for
     1075% the intel MCS-51 microprocessor}.
     1076%   D. P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second
     1077% international conference on Certified Programs and Proofs, Springer-Verlag 2012.
     1078%
     1079% \bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable Real-Time
     1080% Systems}, F.J. Cazorla, E. Qui\~{n}ones, T. Vardanega, L. Cucu, B. Triquet, G.
     1081% Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions
     1082% on Embedded Computing Systems, 2012.
     1083%
     1084% \bibitem{embounded} \textbf{The EmBounded project (project paper)}. K. Hammond,
     1085% R. Dyckhoff, C. Ferdinand, R. Heckmann, M. Hofmann, H. Loidl, G. Michaelson, J.
     1086% Serot, A. Wallace, in Trends in Functional Programming, Volume 6, Intellect
     1087% Press, 2006.
     1088%
     1089% \bibitem{matita}
     1090% \textbf{The Matita Interactive Theorem Prover}.
     1091% A. Asperti, C. Sacerdoti Coen, W. Ricciotti, E. Tassi.
     1092% 23rd International Conference on Automated Deduction, CADE 2011.
     1093%
     1094% \bibitem{typeffects} \textbf{The Type and Effect Discipline}. J.-P. Talpin,
     1095%  P. Jouvelot.
     1096%   In Proceedings of the Seventh Annual Symposium on Logic in Computer Science
     1097% (LICS '92), Santa Cruz, California, USA, June 22-25, 1992.
     1098% IEEE Computer Society 1992.
     1099%
     1100% \bibitem{stateart} \textbf{The worst-case execution-time problem overview of
     1101% methods
     1102% and survey of tools.} R. Wilhelm et al., in  ACM Transactions on Embedded
     1103% Computing Systems, 7:1–53, May 2008.
     1104%
     1105% %\bibitem{proartis2} \textbf{A Cache Design for Probabilistic Real-Time
     1106% % Systems}, L. Kosmidis, J. Abella, E. Quinones, and F. Cazorla, in Design,
     1107% % Automation, and Test in Europe (DATE), Grenoble, France, 03/2013.
     1108%
     1109% \end{thebibliography}
    11101110
    11111111
Note: See TracChangeset for help on using the changeset viewer.