| 1 | | = FraDeCoPP-3 = |
| | 1 | = FraDeCoP-3 -- Third Workshop on Frameworks for the Development of Correct (parallel) Programs = |
| | 2 | |
| | 3 | == Date and Location == |
| | 4 | |
| | 5 | October, 2013, room "Salle de réunion 1" (2nd floor/1er étage) |
| | 6 | |
| | 7 | LIFO, Orléans ([http://www.univ-orleans.fr/lifo/acces.php?lang=fr&sub=sub4 comment venir]) |
| | 8 | |
| | 9 | == Tentative Program == |
| | 10 | |
| | 11 | |
| | 12 | 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. |
| | 13 | |
| | 14 | 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 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. |
| | 15 | |
| | 16 | |
| | 17 | 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. |
| | 18 | The use of proof assistant or automated tools in the process increases the confidence we can have in derived programs. |
| | 19 | |
| | 20 | |
| | 21 | The 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. |
| | 22 | While we are interested in seeing such works applied to parallel programs, works on sequential programs will be considered with a great interest. |
| | 23 | |
| | 24 | Topics of interest include but are not limited to: |
| | 25 | |
| | 26 | * Formal framework for: |
| | 27 | * programs transformation |
| | 28 | * programs refinement |
| | 29 | * "Hoare logic" style proofs of programs |
| | 30 | * programs analysis |
| | 31 | * Experience feedback on the development of "formally proved correct" programs |
| | 32 | |
| | 33 | == Organizers == |
| | 34 | |
| | 35 | * Frédéric Loulergue, Université d'Orléans |
| | 36 | * Thomas Pinsard, Université d'Orléans |
| | 37 | * Julien Tesson, Université Paris-Est |
| | 38 | |
| | 39 | == Past Worshops == |
| | 40 | |
| | 41 | * [wiki:FraDeCoPP-2] |
| | 42 | * [wiki:FraDeCoPP2012] |
