| 25 | | * 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. |
| | 25 | * 16h30-17h30 Jean Fortin (Université Paris Est Créteil), '''[http://frederic.loulergue.eu/ftp/fortin_fradecopp-3.pdf 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. |
