Welcome to SDPP Home Page

SDPP is a framework for Systematic Development of Parallel Programs.

We use the ​Coq proof assistant for systematically derive Bulk Synchronous Parallel ML (or ​BSML) programs.

Team

• Wadoud Bousdira, ​LIFO, ​Université d'Orléans
• Zhenjiang Hu, ​National Institute of Informatics
• Kento Emoto, ​IPL, The University of Tokyo
• Frédéric Loulergue, ​LIFO, ​Université d'Orléans
• Kimironi Matsuzaki, ​Kochi University of Technology
• Julien Tesson, ​LIFO, ​Université d'Orléans

Past members: Louis Gesbert, Hideki Hashimoto, Masato Takeichi, Sylvain Dailler

Software

• Library "Systematic Development of Parallel Programs" and "Certified BSML" ​version 0.2
• Library "Systematic Development of Parallel Programs" ​version 0.1
• Library "Program Calculation in Coq": ​version 0.1, ​version 0.15, ​version 0.16 (for Coq 8.3)

Publications

Conferences

• Joeffrey Legaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, and Julien Tesson. Programming with BSP Homomorphism. In Euro-Par 2013 Parallel Processing, LNCS. Springer, 2013. to appear.
• J. Tesson and F. Loulergue. ​A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation. In 11th International Conference on Computational Science (ICCS 2011), Procedia Computer Science. pages 36-45, Elsevier, 2011.
• L. Gesbert, Z. Hu, F. Loulergue, K. Matsuzaki, and J. Tesson. ​Systematic Development of Correct Bulk Synchronous Parallel Programs. In The 11th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT). IEEE Computer Society, 2010.
• J. Tesson, H. Hashimoto, Z. Hu, F. Loulergue, and M. Takeichi. ​Program Calculation in Coq. In Thirteenth International Conference on Algebraic Methodology And Software Technology (AMAST2010), LNCS 6486, pages 163–179, Springer, 2010
• H. Hashimoto, Z. Hu, J. Tesson, F. Loulergue, and M. Takeichi. ​A Coq Library for Program Calculation. In JSSST Conference on Software Science and Technology, 2009.

Thesis

• Julien Tesson, ​Environnement pour le développement et la preuve de correction systématiques de programmes parallèles fonctionnels. PhD Thesis, LIFO, University of Orléans, November 2011
• Louis Gesbert, ​Développement systématique et sûreté d'exécution en programmation parallèle structurée. PhD thesis, University Paris Est, LACL, 2009

Research reports

• Frédéric Loulergue, Virginia Niculescu, ​Programming and Reasoning with PowerLists in Coq, Research Report RR-2013-02, LIFO, Université d'Orléans, 2013
• Julien Tesson, Zhenjiang Hu, Kiminori Matsuzaki, Frédéric Loulergue and Louis Gesbert, ​Systematic Development of Functional Bulk Synchronous Parallel Programs, Research Report RR-2010-01, LIFO, University of Orléans, 2010
• Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, and Masato Takeichi, ​Program Calculation in Coq, Research Report RR-2009-07, LIFO, University of Orléans, 2009