Formal Semantics of a Subset of the Paderborn's BSPlib. - Frédéric Gava; Jean Fortin (PDCAT, 2008)

Two Formal Semantics of a Subset of the Paderborn University BSPlib. - Frédéric Gava; Jean Fortin (PDP, 2009)

From BSP routines to high-performance ones: Formal verification of a transformation case. - Jean Fortin; Frédéric Gava (ICCS, 2010)

Mechanised Verification of Distributed State-Space Algorithms for Security Protocols. - Frédéric Gava; Arthur Hidalgo; Jean Fortin (PDCAT, 2012)

Deductive Verification of State-Space Algorithms. - Frédéric Gava; Jean Fortin; Michaël Guedj (IFM, 2013)

BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms. (BSP-Why, a tool for deductive verification of BSP programs : sémantiques mécanisées et application aux algorithmes d'espace d'états distribués). - Jean Fortin (2013)

Towards Mechanised Semantics of HPC: The BSP with Subgroup Synchronisation Case. - Jean Fortin; Frédéric Gava (ICA3PP (Workshops and Symposiums), 2015)

BSP-Why: A Tool for Deductive Verification of BSP Algorithms with Subgroup Synchronisation. - Jean Fortin; Frédéric Gava (Int. J. Parallel Program., 2016)