Changes between Version 3 and Version 4 of FraDeCoPP2012


Ignore:
Timestamp:
Apr 7, 2012, 11:35:31 AM (6 years ago)
Author:
julien.tesson@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • FraDeCoPP2012

    v3 v4  
    1313The trend is towards the increase of cores in processors, the number of processors and the need for scalable computing everywhere. But parallel program design and implementation is a complex, error prone task.  Thus there is a need for methods to verify parallel programs or insure their correctness by constructive methods. 
    1414 
    15 In the [http://traclifo.univ-orleans.fr/PaPDAS PaPDAS] project we are interested in providing a framework to ease the development of correct parallel programs in a systematic way using constructive algorithmic. That is, in our case, to construct efficient and correct parallel programs by transformation of simple programs toward a combination of algorithmic skeletons. To insure the correctness of the final implementation '''and''' to keep this implementation efficient means that we need verified efficient implementation of a set of skeletons. 
     15In the [http://traclifo.univ-orleans.fr/PaPDAS PaPDAS] project we are interested in providing a framework to ease the development of correct parallel programs in a systematic way using constructive algorithmic. That is, in our case, to construct efficient and correct parallel programs by transformation of simple programs towards a combination of algorithmic skeletons. Insuring the correctness of the final implementation '''and''' keeping this implementation efficient means that we need verified efficient implementation of a set of skeletons. 
    1616 
    1717 
    1818Formal methods like refinement methods, Hoare logics, embedding of languages in a proof assistant, model checking, static analysis, have proved their usefulness to verify different kind of properties of  programs. Constructive methods allow to construct efficient correct programs by transformation of simpler programs, insuring the preservation of some properties (usually functional correctness) along the process.  
    19 The use of proof assistant or automated tools in the process leverage the confidence we can have in derived programs.  
     19The use of proof assistant or automated tools in the process increases the confidence we can have in derived programs.  
    2020 
    2121 
    22 The FraDeCoP workshop aims to provide an informal and friendly setting to discuss recent work and work in progress on framework for the development of formally verified programs using program transformation, program refinement, or /a posteriori/ proof of correctness, or experience feedback in the use of such framework. 
    23 While we are interested in seeing such work applied to parallel programs, works on sequential programs will be considered with a great interest. 
     22The FraDeCoP workshop aims to provide an informal and friendly setting to discuss recent or ongoing works on framework for the development of formally verified programs using programs transformation, programs refinement, or /a posteriori/ proof of correctness, or experience feedback in the use of such a framework. 
     23While we are interested in seeing such works applied to parallel programs, works on sequential programs will be considered with a great interest. 
    2424 
    2525 
    2626== Topics of interest ==  
    27 includes but are not limited to: 
     27include but are not limited to: 
    2828 
    2929* Formal framework for: 
    … …  
    4040== Talk Proposal == 
    4141 
    42 To propose a talk for the workshop, please email Julien Tesson (tesson.julien_at_kochi-tech.ac.jp) before April 30, 2012, a title and short abstract in plain text or pdf format. 
     42To propose a talk for the workshop, please email Julien Tesson (tesson.julien_at_kochi-tech.ac.jp) before April 30, 2012, a title and a short abstract in plain text or pdf format. 
    4343 
    4444== Organiser == 
    … …  
    4848== Registration == 
    4949 
    50 Registration is free, but it is mandatory to do it before the may 1st. 
     50Registration is free, but it is mandatory to do it before may 1st by sending an e-mail to Julien Tesson (tesson.julien_at_kochi-tech.ac.jp).  
    5151Free lunch and coffe break, travel expenses may be reimbursed if needed (contact us as early as possible).