FraDeCoP 2012 -- Workshop on Frameworks for the Development of Correct (parallel) Programs
Date and Location
FraDeCoP will be held in Université Paris-Est Créteil, France on May 15th, 2012
Salle des thèses
LACL, Bâtiment P2 du CMC,
61 avenue du Général de Gaulle
94010 Créteil Cedex
Université de Paris-Est-Créteil
Program
10:00-10:30 Accueil
10:30-11h15 Kiminori Matsuzaki : Constructive Algorithmic (slides)
11:15-12:00 Julien Tesson : Mechanisation of constructive algorithmic with Coq (slides)
12:00-13:30 Lunch
13:30-14:15 Matthieu Giorgino : Proofs of pointer algorithms by inductive representation of graphs (abstract | slides)
14:15-15:30 Vladimir Komendantsky : Cost analysis for patterns of parallelism (abstract | slides )
15:30-16:00 Coffee break
16:00-16:45 Frédéric Gava : Verification of imperative BSP programs ( slides)
16:45-18:00 Discussion / Démos
Abstracts
Mathieu Giorgino : Proofs of pointer algorithms by inductive representation of graphs
We present a proof method based on the representation of pointer structures as inductive algebraic data-types adorned with additional pointers in a proof-assistant. The advantage is then to be able to apply structural induction principles and other usual techniques available in proof-assistant. We illustrate it on two case-studies: the verification of an algorithm to construct BDDs (Binary Decision Diagrams) and the verification of the Schorr-Waite algorithm.
Vladimir Komendantsky : Cost analysis for patterns of parallelism
Several notions of cost analysis have been introduced in the literature for functional programs that produce structured (a.k.a. shapely) data. Departing from pure data, I propose a higher-order cost analysis for pattern matching programs (skeletons) that produce functional programs. The proposal employs the pattern matching calculus due to Barry Jay. I will illustrate the idea on a divide-and-conquer pattern implementation in that calculus.
Aim and Scope
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.
In the 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.
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. The use of proof assistant or automated tools in the process increases the confidence we can have in derived programs.
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. While we are interested in seeing such works applied to parallel programs, works on sequential programs will be considered with a great interest.
Topics of interest
include but are not limited to:
- Formal framework for:
- programs transformation
- programs refinement
- "Hoare logic" style proofs of programs
- programs analysis
- Experience feedback on the development of "formally proved correct" programs
Talk Proposal
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 a short abstract in plain text or pdf format.
Organiser
Julien Tesson, Kochi University of Technology, Japan.
Kiminori Matsuzaki, Kochi University of Technology, Japan.
Frédéric Gava, Université Paris-est Créteil, France.
Registration
Registration 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).
Free lunch and coffee break, travel expenses may be reimbursed if needed (contact us as early as possible).
