Changeset 1659


Ignore:
Timestamp:
Jan 26, 2012, 8:43:27 AM (6 years ago)
Author:
amadio
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D5.1/report.tex

    r1657 r1659  
    553553\begin{LARGE}
    554554\bf
    555 Report n. D5.1 Untrusted CerCo Prototype \\
     555Report \\
     556D5.1 Untrusted CerCo Prototype \\
    556557and \\
    557558D5.3 Case study: analysis of synchronous code
     
    590591\paragraph{Summary}
    591592The main aim of WP5 is to develop proof of concept prototypes where
    592 the (untrusted) compiler developed in WP 2 is interfaced with existing tools
     593the (untrusted) compiler developed in WP2 is interfaced with existing tools
    593594in order to synthesize complexity  assertions on the execution
    594 time of programs. 
    595 
    596 The main expected contribution (D5.1) is a Frama-C plug-in that takes as
    597 input the annotated C program produced by the CerCo compiler and
    598 tries to synthesize a certified bound on the execution time.
    599 
    600 Because of the redistribution of the workforce in the UDP site
    601 (following the resignation of the doctoral student at the end of year 1
    602 the contract of the post-doc has been extended till month ??) we propose
    603 to anticipate at month 24 instead of month 36 the presentation of
    604 deliverable D5.3 which is consists in particular in applying
    605 the Frama-C plug-in to the C programs generated by a Lustre compiler.
    606 
    607 This work is described in the document ...
    608 
    609 During the second year some unplanned work has taken place.
     595time of programs. Eventually, the approach should be adapted to
     596the trusted compiler developed in WP3 and WP4 (cf. deliverable D5.2 at
     597month 36).
     598
     599In particular, the main planned contribution of deliverable D5.1 is a
     600tool that takes as input an annotated C program produced by the CerCo
     601compiler and tries to synthesize a certified bound on the execution
     602time of the program.  The related expected contribution of deliverable
     603D5.3 amounts to apply the developed tool to the C programs generated
     604by a Lustre compiler.  This planned work is described in the first
     605document...which accompanies a software distribution...
     606Frama-C plug-in ...more examples...
     607
     608We pause to recall a redistribution of the workforce of the UDP site.
     609Following the resignation of the doctoral student at the end of year
     6101, the contract of the post-doc has been as extended till month ??  It
     611follows that in the UPD site there has been a shift of manpower from
     612the third to the second year. Because of this shift we decided to
     613anticipate the presentation of deliverable D5.3 at month 24 rather
     614than month 36.
     615
     616During the second year some unplanned work related to deliverables
     617D5.1 and D5.3 has taken place at UPD.
    610618
    611619The main development concerns the extension of the CerCo labelling
    612 approach to a standard compilation chain from a higher-order functional
    613 language of the ML family to C and the development of framework to reason
    614 about the cost annotations. This work shows...the generality of the approach...
    615 Parallel the work done for C...
    616 Ongoing work tries to produce valid garbage collection statements by typing...
    617 
    618 A second development is concerned with the development of a type system
     620approach to a standard compilation chain from a higher-order
     621functional language of the ML family to C and the development of
     622framework to reason about the cost annotations. This work shows...the
     623generality of the approach...  Parallel the work done for C...
     624Ongoing work tries to produce valid garbage collection statements by
     625typing...
     626
     627A second development is of a more speculative nature and
     628concerned with the development of a type system
    619629for a functional langauge with side effects that guarantees a complexity
    620630bound... First work to account for side effects... Ongoing work tries to
     
    622632the thread on implicit complexity???
    623633
     634
     635
    624636\newpage
    625637
Note: See TracChangeset for help on using the changeset viewer.