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

• Zhenjiang Hu,  National Institute of Informatics and  IPL, The University of Tokyo
• Frédéric Loulergue,  LIFO,  Université d'Orléans
• Julien Tesson,  LIFO,  Université d'Orléans
• Sylvain Dailler,  LIFO,  Université d'Orléans
• Kimironi Matsuzaki,  Kochi University of Technology
• Masato Takeichi,  IPL, The University of Tokyo

Past members: Louis Gesbert, Hideki Hashimoto

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

Journal and conferences

• 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

• 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
• 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

Research reports

• 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