Changeset 3455


Ignore:
Timestamp:
Feb 20, 2014, 4:20:30 PM (6 years ago)
Author:
mulligan
Message:

more space saving. now down to 16 pages + 1 page bibliography

Location:
Papers/fopara2013
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.bib

    r3444 r3455  
    3131volume={7437},
    3232series={LNCS},
    33 editor={Stoelinga, Mariëlle and Pinger, Ralf},
    3433doi={10.1007/978-3-642-32469-7_3},
    3534title={Certifying and Reasoning on Cost Annotations in {C} Programs},
    3635url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
    37 publisher={Springer Berlin Heidelberg},
    3836author={Ayache, Nicolas and Amadio, RobertoM. and R\'egis-Gianas, Yann},
    39 pages={32-46}
     37pages={32--46}
    4038}
    4139
    4240@incollection{labelling2,
    4341year={2012},
    44 isbn={978-3-642-32494-9},
    4542booktitle={Foundational and Practical Aspects of Resource Analysis},
    4643volume={7177},
    4744series={LNCS},
    48 editor={Peña, Ricardo and Eekelen, Marko and Shkaravska, Olha},
    4945doi={10.1007/978-3-642-32495-6_5},
    5046title={Certifying and Reasoning on Cost Annotations of Functional Programs},
    51 url={http://dx.doi.org/10.1007/978-3-642-32495-6_5},
    52 publisher={Springer Berlin Heidelberg},
    5347author={Amadio, RobertoM. and R\'egis-Gianas, Yann},
    54 pages={72-89},
     48pages={72--89},
    5549note={Extended version to appear in Higher Order and Symbolic Computation, 2013}
    5650}
     
    138132  booktitle = {CPP},
    139133  year      = {2012},
    140   pages     = {43-59},
    141   ee        = {http://dx.doi.org/10.1007/978-3-642-35308-6_7},
    142   crossref  = {DBLP:conf/cpp/2012},
    143   bibsource = {DBLP, http://dblp.uni-trier.de}
     134  pages     = {43--59},
     135  doi       = {10.1007/978-3-642-35308-6_7}
    144136}
    145137@proceedings{DBLP:conf/cpp/2012,
     
    191183               September 2005},
    192184  booktitle = {Trends in Functional Programming},
    193   publisher = {Intellect / University of Chicago Press},
    194185  series    = {Trends in Functional Programming},
    195186  volume    = {6},
  • Papers/fopara2013/fopara13.tex

    r3454 r3455  
    181181
    182182\section{Project context and approach}
    183 Formal methods for the verification of functional properties of programs are now sufficiently mature to find increasing application in production environments. For safety critical code, it is commonplace to combine rigorous engineering methodologies and testing
     183Formal methods for the verification of functional properties of programs are now mature enough to find increasing application in production environments. For safety critical code, it is commonplace to combine rigorous engineering methodologies and testing
    184184with static analyses, taking the strengths of each and mitigating
    185185their weaknesses. Of particular interest are open frameworks
     
    209209of hardware design.
    210210
    211 Despite the aforementioned problems, the need for reliable real time
    212 systems and programs is increasing, and there is increasing pressure
    213 from the research community towards the introduction of alternative
     211Despite these problems, the need for reliable real time
     212systems and programs is increasing, and there is a push
     213from the research community towards the introduction of
    214214hardware with more predictable behaviour, which would be more suitable
    215 for static analysis.  One example, being investigated by the Proartis
     215for static analysis.  One example, exemplified by the Proartis
    216216project~\cite{proartis}, is to decouple execution time from execution
    217217history by introducing randomisation.
    218218
    219 In the CerCo project \cite{cerco} we do not try to address this problem, optimistically
     219In CerCo~\cite{cerco} we do not address this problem, optimistically
    220220assuming that improvements in low-level timing analysis or architecture will make
    221221verification feasible in the longer term. Instead, the main objective of our work is
    222222to bring together the static analysis of functional and non-functional
    223 properties, which, according to the current state of the art, are completely
     223properties, which in the current state of the art are
    224224independent activities with limited exchange of information: while the
    225225functional properties are verified on the source code, the analysis of
    226 non-functional properties is entirely performed on the object code to exploit
     226non-functional properties is performed on object code to exploit
    227227clock-precise hardware models.
    228228
     
    232232First, there cannot be a uniform, precise cost model for source
    233233code instructions (or even basic blocks). During compilation, high level
    234 instructions are torn apart and reassembled in context-specific ways so that
     234instructions are disassembled and reassembled in context-specific ways so that
    235235identifying a fragment of object code and a single high level instruction is
    236236infeasible. Even the control flow of the object and source code can be very
     
    745745\subsection{The CerCo C compilers}
    746746We implemented two C compilers, one implemented directly in OCaml and
    747 the other implemented in the interactive theorem prover
    748 Matita~\cite{matita}.  The first acted as a prototype for the second,
     747the other implemented in Matita, an interactive theorem prover~\cite{matita}.  The first acted as a prototype for the second,
    749748but also supported MIPS and acted as a testbed for more advanced
    750749features such as the dependent labelling approach
     
    782781of a compiler from Pascal to MIPS used by Fran\c{c}ois Pottier for a course at the
    783782\'{E}cole Polytechnique.
    784 
    785783The main differences in the CerCo compiler are:
    786 \begin{enumerate}
     784\begin{itemize*}
    787785\item All the intermediate languages include label emitting instructions to
    788786implement the labelling approach, and the compiler preserves execution traces.
     
    807805%support full recursion in order to test the CerCo tools also on recursive
    808806%programs, the compiler implements a stack in external memory.
    809 \end{enumerate}
     807\end{itemize*}
    810808
    811809\subsection{Formal certification of the CerCo compiler}
    812810We have formally
    813 certified in the Matita interactive proof assistant that the cost models induced on the source code by the
     811certified in Matita that the cost models induced on the source code by the
    814812Trusted CerCo Compiler correctly and precisely
    815813predict the object code behaviour. There are two cost models, one for execution
     
    985983\paragraph{The Cost plugin and its application to the Lustre compiler.}
    986984Frama-C \cite{framac} is a set of analysers for C programs with a
    987 specification language called ACSL. New analyses can be dynamically added
    988 via a plugin system. For instance, the Jessie plugin~\cite{jessie} allows deductive
     985specification language, ACSL. New analyses can be added dynamically
     986via plugins. For instance, the Jessie plugin~\cite{jessie} allows deductive
    989987verification of C programs with respect to their specification in ACSL, with
    990988various provers as back-end tools.
     
    10551053loop. An axiom is added to account for the fact that the cost is accumulated at each
    10561054step of the loop.
    1057 The cost of the function is directly added as post-condition of the function.
     1055The cost of the function is added as post-condition of the function.
    10581056
    10591057The user can also specify more precise variants and annotate functions
     
    10731071
    10741072\paragraph{C programs with pointers.}
    1075 When it comes to verifying programs involving pointer-based data structures,
    1076 such as linked lists, trees, or graphs, the use of traditional first-order logic
    1077 to specify, and of SMT solvers to verify, shows some limitations. Separation
    1078 logic is an elegant alternative. It is a program logic
    1079 with a new notion of conjunction to express spatial heap separation. Bobot has
     1073Using first-order logic and SMT solvers to specify and verify programs involving pointer-based
     1074data structures such as linked-lists or graphs shows some limitations.
     1075Separation logic, a program logic
     1076with a new notion of conjunction to express spatial heap separation, is an elegant alternative.
     1077Bobot has
    10801078recently introduced automatically generated separation
    10811079predicates to simulate separation logic reasoning in the Jessie plugin where the specification language, the verification condition
    10821080generator, and the theorem provers were not designed with separation logic in
    1083 mind~\cite{bobot}. CerCo's plugin can exploit the separation predicates to automatically
    1084 reason on the cost of execution of simple heap manipulation programs such as an
     1081mind~\cite{bobot}. CerCo's plugin can exploit these predicates to automatically
     1082reason about the cost of execution of simple heap manipulation programs such as an
    10851083in-place list reversal.
    10861084
Note: See TracChangeset for help on using the changeset viewer.