| | 1 | = FraDeCoP 2012 -- Workshop on Frameworks for the Development of Correct (parallel) Programs = |
| | 2 | |
| | 3 | == Date and Location == |
| | 4 | |
| | 5 | FraDeCoP will be held in Paris, France on May 2012 |
| | 6 | |
| | 7 | == Program == |
| | 8 | |
| | 9 | TBA |
| | 10 | |
| | 11 | == Aim and Scope == |
| | 12 | |
| | 13 | The 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. |
| | 14 | |
| | 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. |
| | 16 | |
| | 17 | |
| | 18 | Formal 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. |
| | 20 | |
| | 21 | |
| | 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. |
| | 24 | |
| | 25 | |
| | 26 | == Topics of interest == |
| | 27 | includes but are not limited to: |
| | 28 | |
| | 29 | - Framework for: |
| | 30 | * programs transformation |
| | 31 | * programs refinement |
| | 32 | * "Hoare logic" style proofs of programs |
| | 33 | * programs analysis |
| | 34 | |
| | 35 | - Experience feedback on the development of "formally proved correct" programs |
| | 36 | |
| | 37 | |
| | 38 | |
| | 39 | |
| | 40 | == Talk Proposal == |
| | 41 | |
| | 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. |
| | 43 | |
| | 44 | == Organiser == |
| | 45 | |
| | 46 | Julien Tesson, Kochi University of Technology |
| | 47 | |
| | 48 | == Registration == |
| | 49 | |
| | 50 | Registration is free, but mandatory. |
| | 51 | |
| | 52 | Si JST est ok: |
| | 53 | Lunch will be offered, travel expenses may be reimbursed if needed (contact us as early as possible). |
