Changes between Version 7 and Version 8 of FraDeCoPP-3

Timestamp:

Sep 18, 2013, 5:07:16 PM (5 years ago)

Author:

frederic.loulergue@…

Comment:

--

FraDeCoPP-3

@@ -17 +17 @@
 * 12h00-14h00 '''Déjeuner / Lunch (Restaurant l'Agora)''' 
 
-* 14h00-15h00 Rita Loogen (Philipps-Universität Marburg), '''Parallel Functional Programming in Eden'''[[BR]]
+* 14h00-15h00 Rita Loogen (Philipps-Universität Marburg), '''Parallel Functional Programming in Eden'''[[BR]]Eden extends Haskell with constructs for the definition and instantiation of parallel processes. Processes evaluate function applications remotely in parallel. The programmer has control over process granularity, data distribution, communication topology, and evaluation site, but need not manage synchronisation and data exchange between processes. The latter are performed by the parallel runtime system through implicit communication channels, transparent to the programmer. Common and sophisticated parallel communication patterns and topologies, so-called algorithmic skeletons, are provided as higher-order functions in a user-extensible skeleton library written in Eden. Eden is geared toward distributed settings, i.e.\ processes do not share any data, but can equally well be used on multicore systems. In the talk, we give an introduction into Eden's language constructs and its skeleton-based programming methodology. 
 
 * 15h00-16h00 Yolanda Ortega-Mallén (Universidad Complutense de Madrid), '''Formal Semantics for the Parallel Language Eden'''[[BR]]We present two formal semantics for the kernel of the parallel language Eden. First we describe an operational semantics expressed as a two-level transition system. Next we present a denotational semantics based on continuations, suitable for dealing with side-effects and parallelism. We end by comparing both approaches.
@@ -23 +23 @@
 * 16h00-16h30 '''Pause / Coffee Break'''
 
-* 16h30-17h30 Jean Fortin (Université Paris Est Créteil), ''' BSP-Why: a Tool for Deductive Verification of BSP Programs'''[[BR]]
+* 16h30-17h30 Jean Fortin (Université Paris Est Créteil), ''' BSP-Why: a Tool for Deductive Verification of BSP Programs'''[[BR]]This presentation is based on the author's Doctoral thesis and falls within the formal verification of parallel programs. The aim of formal verification is to ensure that a program will run as it should, without making mistakes, blocking, or terminating abnormally. This is even more important in the parallel computation field, where the cost of calculations can be very high. The BSP model (Bulk Synchronous Parallelism) is a model of parallelism well suited for the use of formal methods. It guarantees a structure in the parallel program, by organising it into super-steps, each of them consisting in a phase of computations, followed by communications between the processes. In this thesis, we chose to extend an existing tool to adapt it for the proof of BSP programs. We based our work on WHY, a VCG (verification condition generator) that has the advantage of being able to interface with several automatic provers and proof assistants to discharge the proof obligations. There are multiple contributions in this thesis. In a first part, we present a comparison of the existing BSP libraries, in order to show the most used BSP primitives, which are the most interesting to formalise. We then present BSP-WHY, our tool for the proof of BSP programs. This tool generates a sequential program to simulate the parallel program in input, thus allowing the use of why and the numerous associated provers to solve the proof obligations. We then show how BSP-WHY can be used to prove the correctness of some basic BSP algorithms. We also present a more complex example, the generation of the state-space (model-checking) of systems, especially for security protocols. Finally, in order to ensure the greatest
+confidence in the BSP-WHY tool, we give a formalisation of the language semantics, in the coq proof assistant. We also prove the correctness of the transformation used to go from a parallel program to a sequential program.
 
 * 17h30-18h00 '''Conclusion'''