Publications

2024

[hal-04528312] Wolfgang Ahrendt, Frédéric Loulergue, Heike Wehrheim,
Introduction to the Special Collection from the International Conference on Tests and Proofs (TAP) 2020 and 2021
Formal Aspects of Computing, 36 (1), pp.1-2, 2024, ⟨10.1145/3650092⟩

[hal-04597523] Frédéric Loulergue, Julien Tesson,
Verified Parallel Programming in Coq with Bulk Synchronous Parallel Homomorphisms
17th International Symposium on High-Level Parallel Programming and Applications (HLPP), Jul 2024, Pisa, Italy

[hal-04556201] Frédéric Loulergue, Olivia Proust,
WhyBSML 0.2
2024, ⟨swh:1:dir:f3889ab751233d7ccb812d6e31cc074452b5e139;origin=https://hal.archives-ouvertes.fr/hal-04556201;visit=swh:1:snp:eb9686bbb19def3cd7e40be139923aa5270faed8;anchor=swh:1:rel:0040e1fae30354391bea7e4b4fc245556353fd87;path=/⟩

[hal-04354615] Téo Bernier, Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue,
Combining Deductive Verification with Shape Analysis
27th International Conference on Fundamental Approaches to Software Engineering (FASE), 2024, Luxembourg, Luxembourg. pp.280-289, ⟨10.1007/978-3-031-57259-3_14⟩

[hal-04605772] Yohan Boichut, Adrien Boiret, Vincent Hugot,
SAT-Based Automated Completion for Reachability Analysis
International Conference on Implementation and Application of Automata, 2024

[hal-04572043] Farid Arfi, Hélène Coullon, Frédéric Loulergue, Jolan Philippe, Simon Robillard,
An Overview of the Decentralized Reconfiguration Language Concerto-D through its Maude Formalization
ICE 2024 - 17th Interaction and Concurrency Experience, Jun 2024, Groningen, Netherlands

[hal-04067909] Hélène Coullon, Ludovic Henrio, Frédéric Loulergue, Simon Robillard,
Component-Based Distributed Software Reconfiguration: a Verification-Oriented Survey
ACM Computing Surveys, 2024, 56 (1), pp.1-37. ⟨10.1145/3595376⟩

[hal-04065774] Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles,
Sound runtime assertion checking for memory properties via program transformation
Formal Aspects of Computing, 2024, 36 (1), pp.4:1-46. ⟨10.1145/3605951⟩


2023

[hal-04142453] Frédéric Loulergue, Jolan Philippe,
Towards Verified Scalable Parallel Computing with Coq and Spark
Workshop on Formal Techniques for Java-like Programs (FTfJP), Jul 2023, Seatle, WA, United States. ⟨10.1145/3605156.3606450⟩

[hal-04173428] Olivia Proust, Frédéric Loulergue,
Verified Scalable Parallel Computing with Why3
21st International Conference on Software Engineering and Formal Methods (SEFM), Nov 2023, Eindhoven, Netherlands. ⟨10.1007/978-3-031-47115-5_14⟩

[hal-04171949] Frédéric Loulergue, Abdelali Ed-Dbali,
Verified High Performance Computing: the SyDPaCC Approach
16th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS), Oct 2023, Marrakech, Morocco. ⟨10.1007/978-3-031-49737-7_2⟩

[hal-03995588] Virginia Niculescu, Frédéric Loulergue,
Guest Editor’s Note: High-Level Parallel Programming 2021
International Journal of Parallel Programming, 2023, ⟨10.1007/s10766-023-00752-x⟩

[hal-04142455] Darine Rammal, Wadoud Bousdira, Frederic Dabrowski,
Synchronous cooperative threading model in MSSL
SAC '23: 38th ACM/SIGAPP Symposium on Applied Computing, 2023, Tallinn, Estonia. pp.1380-1383, ⟨10.1145/3555776.3577815⟩

[hal-04176159] Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, Téo Bernier,
Towards Formal Verification of a TPM Software Stack
18th International Conference on integrated Formal Methods (iFM), Nov 2023, Leiden, Netherlands. ⟨10.1007/978-3-031-47705-8_6⟩

[hal-04142454] Frédéric Loulergue,
Tutorial: Collaborative Analysis and Verification of C Programs with Frama-C
38th IEEE/ACM International Conference on Automated Software Engineering (ASE), Sep 2023, Kirchberg, Luxembourg


2022

[hal-03356610] Nirina Andrianarivelo, Pierre Réty,
Modular termination of prefix-constrained term rewrite systems
Information Processing Letters, 2022, ⟨10.1016/j.ipl.2021.106207⟩

[hal-03767722] Siva Anantharaman, Sabine Frittella, Benjamin Nguyen,
Privacy Analysis with a Distributed Transition System and a Data-Wise Metric
Privacy in Statistical Databases (PSD), Sep 2022, PARIS, France. pp.15--30

[hal-03623522] Siva Anantharaman, Sabine Frittella, Benjamin Nguyen,
Distributed Transition Systems with Tags for Privacy Analysis
2022


2021

[hal-03517397] Jules Chouquet, Lionel Vaux,
An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets
Logical Methods in Computer Science, 2021, Volume 17, Issue 4, ⟨10.46298/lmcs-17(4:22)2021⟩

[hal-03160688] Virginia Niculescu, Frédéric Loulergue, Adrian Sterca,
Reflection on the Design of Parallel Programming Frameworks
Evaluation of Novel Approaches to Software Engineering, pp.154-181, 2021, ⟨10.1007/978-3-030-70006-5_7⟩

[hal-03338928] Salwa Souaf, Frédéric Loulergue,
Experience report: Teaching code analysis and verification using Frama-C
1st International Workshop on Applicable Formal Methods (appFM), Nov 2021, Beijing, China. ⟨10.4204/EPTCS.349.5⟩

[hal-03261865] Frédéric Loulergue, Franz Wotawa,
Tests and Proofs
Springer, 12740, 2021, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-79379-1⟩

[hal-03178944] Frederic Dabrowski,
On Single-Valuedness in Textually Aligned SPMD Programs
International Journal of Parallel Programming, 2021, International Journal of Parallel Programming, ⟨10.1007/s10766-021-00710-5⟩


2020

[cea-02879211] Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles,
Verified Runtime Assertion Checking for Memory Properties
TAP 2020 - 14th International Conference on Tests and Proofs, Jun 2020, Bergen, Norway. ⟨10.1007/978-3-030-50995-8_6⟩

[hal-02317068] Virginia Niculescu, Frédéric Loulergue,
Transforming powerlist-based divide-and-conquer programs for an improved execution model
Journal of Supercomputing, 2020, 76 (7), pp.22. ⟨10.1007/s11227-019-02820-x⟩

[hal-03102811] Frédéric Loulergue,
Special Issue of the Journal of Logical and Algebraic Methods in Programming on Formal Approaches to Parallel and Distributed Systems 2018
Journal of Logical and Algebraic Methods in Programming, 116, Elsevier, pp.100580, 2020, ⟨10.1016/j.jlamp.2020.100580⟩

[hal-02494416] Virginia Niculescu, Frédéric Loulergue, Darius Bufnea, Adrian Sterca,
Pattern-driven Design of a Multiparadigm Parallel Programming Framework
13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), 2020, Prague, Czech Republic. ⟨10.5220/0009344100500061⟩

[hal-02870592] Frederic Dabrowski,
Verification of DRMA communications
High-level Parallel Programming and Applications, Jul 2020, Porto, Portugal

[hal-03628124] Frederic Dabrowski,
The Journal of Supercomputing volume 76, page 4976 (2020)
2020


2019

[hal-02018651] Wadoud Bousdira, Arvid Jakobsson, Frederic Dabrowski,
Safe Usage of Registers in BSPlib
SAC 2019, Apr 2019, Limassol, Cyprus. ⟨10.1145/3297280.3297421⟩

[hal-01955283] Arvid Jakobsson, Frederic Dabrowski, Wadoud Bousdira,
Safe Usage of Registers in BSPlib (Preprint)
2019

[hal-03377146] Yohan Boichut, Jean-Michel Couvreur, Xavier Ferry, Mohamadou Tafsir Sakho,
Modeling Concurrent Behaviors as Words
Verification and Evaluation of Computer and Communication Systems, 11847, Springer International Publishing, pp.1-15, 2019, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-35092-5_1⟩

[hal-03622785] Dara Ly, Nikolai Kosmatov, Julien Signoles, Frédéric Loulergue,
Soundness of a Dataflow Analysis for Memory Monitoring
Ada Letters, 2019, 38 (2), pp.97-108. ⟨10.1145/3375408.3375416⟩

[hal-01521746] Yohan Boichut, Jacques Chabin, Pierre Réty,
Towards more precise rewriting approximations
Journal of Computer and System Sciences, 2019, 104, pp.131-148

[hal-02162234] Wadoud Bousdira,
Transforming non textually aligned SPMD programs into textually aligned SPMD programs by using rewriting rules
IEEE/ACM International Conference on High Performance Computing & Simulation, Jul 2019, Dublin, Ireland. pp.982-989

[hal-02123709] Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michaël Rusinowitch,
Unification modulo Lists with Reverse, Relation with Certain Word Equations
CADE-27 - The 27th International Conference on Automated Deduction, Association for Automated Reasoning (AAR), Aug 2019, Natal, Brazil. pp.1--17, ⟨10.1007/978-3-030-29436-6_1⟩

[tel-03215462] Thibaut Tachon,
Automatic Generation of Bulk-Synchronous Parallel code
Distributed, Parallel, and Cluster Computing [cs.DC]. Université d'Orléans, 2019. English. ⟨NNT : 2019ORLE3098⟩

[hal-02123648] Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michael Rusinowitch,
Unification modulo Lists with Reverse as Solving Simple Sets of Word Equations
[Research Report] LIFO, Université d'Orléans; INSA, Centre Val de Loire. 2019

[hal-02317127] Jolan Philippe, Frédéric Loulergue,
PySke: Algorithmic Skeletons for Python
The 2019 International Conference on High Performance Computing & Simulation (HPCS), Jul 2019, Dublin, Ireland. ⟨10.1109/HPCS48598.2019.9188151⟩

[hal-02317074] Jolan Philippe, Frédéric Loulergue,
Parallel programming with Coq: Map and reduce skeletons on trees
34th ACM/SIGAPP Symposium on Applied Computing (SAC), Apr 2019, Limassol, Cyprus. pp.1578-1581, ⟨10.1145/3297280.3299742⟩

[hal-02317055] Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov,
Towards Full Proof Automation in Frama-C Using Auto-active Verification
NFM 2019 - 11th Annual NASA Formal Methods Symposium, May 2019, Houston, TX, United States. pp.88-105, ⟨10.1007/978-3-030-20652-9_6⟩

[hal-02318361] Jolan Philippe, Frédéric Loulergue,
Towards automatically optimizing PySke programs (poster)
International Conference on High Performance Computing and Simulation (HPCS), Jul 2019, Dublin, Ireland. ⟨10.1109/HPCS48598.2019.9188160⟩

[hal-02317118] Salwa Souaf, Frédéric Loulergue,
A First Step in the Translation of Alloy to Coq
21st International Conference on Formal Engineering Methods (ICFEM), 2019, Shenzen, China. ⟨10.1007/978-3-030-32409-4_28⟩

[hal-02317143] Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,
La logique contre les fantômes: comparaison de deux approches pour la preuve d'un module de listes chaînées *
18e journées Approches Formelles dans l'Assistance au Développement de Logic (AFADL), Jun 2019, Toulouse, France.

[tel-02920363] Filip Jakobsson,
Static Analysis for BSPlib Programs
Distributed, Parallel, and Cluster Computing [cs.DC]. Université d'Orléans, 2019. English. ⟨NNT : 2019ORLE2005⟩

[hal-02100515] Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,
Logic against Ghosts: Comparison of Two Proof Approaches for a List Module
SAC 2019 - The 34th ACM/SIGAPP Symposium On Applied Computing, Apr 2019, Limassol, Cyprus. ⟨10.1145/3297280.3297495⟩

[hal-02317123] Frédéric Loulergue, Jolan Philippe,
Automatic Optimization of Python Skeletal Parallel Programs
19th International Conference on Algorithms and Architectures for Parallel Processing (ICA3PP), Dec 2019, Melbourne, Australia. ⟨10.1007/978-3-030-38991-8_13⟩

[hal-02317124] Frédéric Loulergue, Jolan Philippe,
New List Skeletons for the Python Skeleton Library
PDCAT 2019: 20th International Conference on Parallel and Distributed Computing, Applications and Technologies, Dec 2019, Gold Coast, Australia. ⟨10.1109/PDCAT46702.2019.00077⟩

[hal-02018652] Frederic Dabrowski,
A denotational semantics of textually aligned SPMD Program
Journal of Logical and Algebraic Methods in Programming, 2019, ⟨10.1016/j.jlamp.2019.02.010⟩


2018

[hal-01780553] Nirina Andrianarivelo, Pierre Rety,
Confluence of Prefix-Constrained Rewrite Systems
3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Jul 2018, Oxford, United Kingdom

[hal-01903092] Yohan Boichut, Vivien Pelletier, Pierre Rety,
Approximating any Logic Program by a CS-Program
Rewriting Logic and Its Applications - 12th International Workshop, Apr 2018, Thessalonique, Greece. pp.245--260

[hal-01818140] Arvid Jakobsson,
Automatic Cost Analysis for Imperative BSP Programs
International Journal of Parallel Programming, 2018, ⟨10.1007/s10766-018-0562-1⟩

[hal-01819035] Gaétan Hains, Arvid Jakobsson, Youry Khmelevsky,
Towards formal methods and software engineering for deep learning: Security, safety and productivity for dl systems development
2018 Annual IEEE International Systems Conference (SysCon), Apr 2018, Vancouver, France. ⟨10.1109/SYSCON.2018.8369576⟩

[cea-02283406] Dara Ly, Nikolai Kosmatov, Julien Signoles, Frédéric Loulergue,
Soundness of a Dataflow Analysis for Memory Monitoring
HILT 2018 Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems, Nov 2018, Boston, United States. ⟨10.1145/3375408.3375416⟩

[hal-01643971] Frederic Dabrowski,
Textual Alignment in SPMD Programs
SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing, Apr 2018, Pau, France. ⟨10.1145/3167132.3167254⟩

[hal-01785110] Frédéric Dabrowski,
A Denotational Semantics of Textually Aligned SPMD Programs
International Conference on High Performance Computing & Simulation, Jul 2018, Orléans, France. ⟨10.1109/HPCS.2018.00119⟩

[hal-01720401] Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C
Tenth NASA Formal Methods Symposium - NFM 2018, Apr 2018, Newport News, United States. ⟨10.1007/978-3-319-77935-5_3⟩

[hal-02317078] Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,
A Lesson on Verification of IoT Software with Frama-C
2018 International Conference on High Performance Computing & Simulation (HPCS), Jul 2018, Orleans, France. pp.21-30, ⟨10.1109/HPCS.2018.00018⟩

[hal-01811922] Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov,
Ghosts for Lists: from Axiomatic to Executable Specifications
TAP 2018 - 12th International Conference on Tests and Proofs, Jun 2018, Toulouse, France. ⟨10.1007/978-3-319-92994-1_11⟩

[hal-01811932] Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,
Des listes et leurs fantômes : vérification d'un module critique de Contiki avec FRAMA-C
17èmes Journées AFADL : Approches Formelles Dans L'assistance Au Développement De Logiciels, Jun 2018, Toulouse, France

[hal-01777123] Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,
MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory Models
Computer Languages, Systems and Structures, 2018, 53, pp.121-142. ⟨10.1016/j.cl.2018.03.002⟩


2017

[hal-01494832] Arvid Jakobsson, Frederic Dabrowski, Wadoud Bousdira, Frédéric Loulergue, Gaetan Hains,
Replicated Synchronization for Imperative BSP Programs
International Conference on Computational Science (ICCS), 2017, Zürich, Switzerland. ⟨10.1016/j.procs.2017.05.123⟩

[hal-02317110] Jolan Philippe, Wadoud Bousdira, Frédéric Loulergue,
Formalization of a Big Graph API in Coq
2017 International Conference on High Performance Computing & Simulation (HPCS), Jul 2017, Genoa, France. IEEE, 108, pp.893-894, 2017, ⟨10.1109/HPCS.2017.140⟩

[hal-01159182] Frédéric Loulergue, Wadoud Bousdira, Julien Tesson,
Calculating Parallel Programs in Coq using List Homomorphisms
International Journal of Parallel Programming, 2017, 45 (2), pp.300-319. ⟨10.1007/s10766-016-0415-8⟩

[hal-01495453] Thibaut Tachon, Chong Li, Gaétan Hains, Frédéric Loulergue,
Automated generation of BSP automata
Parallel Processing Letters, 2017, 17 (1), ⟨10.1142/S0129626417400023⟩

[hal-01495454] Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov,
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
Fifth International Workshop on Verification and Program Transformation (VPT 2017), Apr 2017, Uppsala, Sweden. ⟨10.4204/EPTCS.253.9⟩

[hal-01445668] Nirina Andrianarivelo, Vivien Pelletier, Pierre Réty,
Transforming Prefix-Constrained or Controlled Rewrite Systems
8th International Symposium on Symbolic Computation in Software Science (SCSS 2017), Apr 2017, Gammarth, Tunisia

[hal-02317112] Christopher Whitney, Frédéric Loulergue,
Towards a Verified Parallel Implementation of Frequent Itemset Mining
2017 International Conference on High Performance Computing & Simulation (HPCS), Jul 2017, Genoa, Italy. IEEE, pp.889-890, ⟨10.1109/HPCS.2017.138⟩

[hal-02317099] Frédéric Loulergue,
Implementing Algorithmic Skeletons with Bulk Synchronous Parallel ML
2017 18th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT), Dec 2017, Taipei, Taiwan. pp.461-468, ⟨10.1109/PDCAT.2017.00079⟩

[hal-02317101] Virginia Niculescu, Frédéric Loulergue, Darius Bufnea, Adrian Sterca,
A Java Framework for High Level Parallel Programming Using Powerlists
2017 18th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT), Dec 2017, Taipei, France. pp.255-262, ⟨10.1109/PDCAT.2017.00049⟩

[hal-02317103] Frédéric Loulergue,
A BSPlib-style API for Bulk Synchronous Parallel ML
Scalable Computing: Practice and Experience, 2017, 18 (3), ⟨10.12694/scpe.v18i3.1306⟩

[hal-02317113] Frédéric Loulergue,
Special Issue of Scalable Computing: Practice and Experience on Practical Aspects of High-Level Parallel Programming
Scalable Computing: Practice and Experience, 18 (1), 2017, Scalable Computing: Practice and Experience, ⟨10.12694/scpe.v18i1.1229⟩

[hal-01495456] Frédéric Loulergue,
Imperative BSPlib-style Communications in Bulk Synchronous Parallel ML
International Conference on Computational Science, Jun 2017, Zurich, Switzerland. ⟨10.1016/j.procs.2017.05.267⟩

[hal-02317096] Frédéric Loulergue,
A Verified Accumulate Algorithmic Skeleton
2017 Fifth International Symposium on Computing and Networking (CANDAR), Nov 2017, Aomori, France. pp.420-426, ⟨10.1109/CANDAR.2017.108⟩

[hal-01944569] Jean-Michel Couvreur, Joaquín Ezpeleta,
A Linear Temporal Logic Model Checking Method over Finite Words with Correlated Transition Attributes
7th International Symposium on Data-Driven Process Discovery and Analysis (SIMPDA), Dec 2017, Neuchâtel, Switzerland. pp.89-104, ⟨10.1007/978-3-030-11638-5_5⟩

[hal-01559832] Frederic Dabrowski,
Textual Alignment in SPMD Programs
[Research Report] RR-2017-07, LIFO, Université d'Orléans. 2017


2016

[hal-01291393] Yohan Boichut, Pierre Réty, Vivien Pelletier,
Synchronized Tree Languages for Reachability in Non-right-linear Term Rewrite Systems
International Workshop on Rewriting Logic and its Applications, Apr 2016, Eindhoven, Netherlands

[hal-01318432] Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,
A CHR-Based Solver for Weak Memory Behaviors
7th Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA), Jul 2016, Saarbrücken, Germany

[hal-01423641] Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue,
Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs
2016 IEEE 16th International Working Conference on Source Code Analysis and Manipulation (SCAM), 2016, Raleigh, NC, United States. pp.6, ⟨10.1109/SCAM.2016.18⟩

[hal-01319565] Thibaut Tachon, Gaétan Hains, Frédéric Loulergue, Chong Li,
Automated generation of BSP automata
High Level Parallel Programming and Applications (HLPP), Jul 2016, Münster, Germany


2015

[hal-01107296] Frédéric Loulergue, Wadoud Bousdira, Julien Tesson,
Calcul de programmes parallèles avec Coq
Informatique Mathématique, CNRS Éditions, 2015, collection Alpha

[hal-01143199] Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard,
A formal semantics of nested atomic sections with thread escape
Computer Languages, Systems and Structures, 2015, 42 (supl), pp.2-21. ⟨10.1016/j.cl.2015.04.001⟩

[hal-01105093] Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard,
Nested atomic sections with thread escape: Compilation to threads and locks
ACM Symposium on Applied Computing (SAC), Apr 2015, Salamanca, Spain

[hal-01225332] Nirina Andrianarivelo, Pierre Réty,
Over-Approximating Terms Reachable by Context-Sensitive Rewriting
Reachability Problems - 9th International Workshop RP 2015, Sep 2015, Varsaw, Poland

[hal-01135918] Yohan Boichut, Jacques Chabin, Pierre Réty,
Towards More Precise Rewriting Approximations
Proceedings of Language and Automata Theory and Applications (LATA), Mar 2015, Nice, France

[hal-01158137] Frédéric Loulergue,
Construction de programmes parallèles en Coq avec des homomorphismes de listes
14èmes journées Approches Formelles dans l'Assistance au Développement Logiciel (AFADL), 2015, Bordeaux, France

[hal-01158134] Asma Guesmi, Patrice Clemente, Frédéric Loulergue, Pascal Berthomé,
Cloud Resources Placement Based on Functional and Non-Functional Requirements
SECRYPT, Jul 2015, Colmar, France

[cea-01834977] Allan Blanchard, N. Kosmatov, M. Lemerre, Frédéric Loulergue,
A case study on formal verification of the anaxagoros hypervisor paging system with frama-C
FMICS 2015 - Formal Methods for Industrial Critical Systems, Jun 2015, Oslo, Norway. pp.15-30, ⟨10.1007/978-3-319-19458-5_2⟩

[hal-01158138] Frédéric Loulergue,
Modèles fonctionnels de MapReduce en Coq
Journées Nationales du GdR GPL, 2015, Bordeaux, France