Frédéric Loulergue

122 papers A 1B 7C 16Misc 20Journal 28Unranked 48

Year	Rank	Type	Title / Venue / Authors
2025	Misc	`conf`	A Mechanized Formalization of an FRP Language with Effects. SAC Jordan Ischard, Frédéric Dabrowski, Jules Chouquet, Frédéric Loulergue
2025	J	`jnl`	Towards Formal Verification of a TPM Software Stack: Achievements and Opportunities. Formal Aspects Comput. Yani Ziani, Téo Bernier, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez
2024	—	`conf`	An Overview of the Decentralized Reconfiguration Language Concerto-D through its Maude Formalization. ICE Farid Arfi, Hélène Coullon, Frédéric Loulergue, Jolan Philippe, Simon Robillard
2024	B	`conf`	Combining Deductive Verification with Shape Analysis. FASE Téo Bernier, Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue
2024	J	`jnl`	Component-based Distributed Software Reconfiguration:A Verification-oriented Survey. ACM Comput. Surv. Hélène Coullon, Ludovic Henrio, Frédéric Loulergue, Simon Robillard
2024	J	`jnl`	Introduction to the Special Collection from the International Conference on Tests and Proofs (TAP) 2020 and 2021. Formal Aspects Comput. Wolfgang Ahrendt, Frédéric Loulergue, Heike Wehrheim
2024	C	`conf`	Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack. TAP Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez
2024	J	`jnl`	Sound Runtime Assertion Checking for Memory Properties via Program Transformation. Formal Aspects Comput. Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles
2024	—	`conf`	SyDPaCC: A Framework for the Development of Verified Scalable Parallel Functional Programs. ISoLA (3) Frédéric Loulergue, Jordan Ischard
2023	J	`jnl`	Guest Editor's Note: High-Level Parallel Programming 2021. Int. J. Parallel Program. Virginia Niculescu, Frédéric Loulergue
2023	B	`conf`	Towards Formal Verification of a TPM Software Stack. iFM Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, Téo Bernier
2023	J	`jnl`	Towards Formal Verification of a TPM Software Stack. CoRR Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, Téo Bernier
2023	—	`conf`	Towards Verified Scalable Parallel Computing with Coq and Spark. FTfJP@ECOOP Frédéric Loulergue, Jolan Philippe
2023	C	`conf`	Verified High Performance Computing: The SyDPaCC Approach. VECoS Frédéric Loulergue, Ali Ed-Dbali
2023	B	`conf`	Verified Scalable Parallel Computing with Why3. SEFM Olivia Proust, Frédéric Loulergue
2023	J	`jnl`	Verified Scalable Parallel Computing with Why3. CoRR Olivia Proust, Frédéric Loulergue
2021	—	`conf`	Experience Report: Teaching Code Analysis and Verification Using Frama-C. AppFM@FM Salwa Souaf, Frédéric Loulergue
2021	—	`ed.`	Tests and Proofs - 15th International Conference, TAP 2021, Held as Part of STAF 2021, Virtual Event, June 21-22, 2021, Proceedings TAP@STAF Frédéric Loulergue, Franz Wotawa
2020	B	`conf`	Pattern-driven Design of a Multiparadigm Parallel Programming Framework. ENASE Virginia Niculescu, Frédéric Loulergue, Darius Bufnea, Adrian Sterca
2020	J	`jnl`	Preface to the special issue on Formal Approaches to Parallel and Distributed Systems 2018. J. Log. Algebraic Methods Program. Frédéric Loulergue
2020	—	`conf`	Reflections on the Design of Parallel Programming Frameworks. ENASE (Selected Papers) Virginia Niculescu, Adrian Sterca, Frédéric Loulergue
2020	J	`jnl`	Transforming powerlist-based divide-and-conquer programs for an improved execution model. J. Supercomput. Virginia Niculescu, Frédéric Loulergue
2020	—	`conf`	Verified Runtime Assertion Checking for Memory Properties. TAP@STAF Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles
2019	C	`conf`	A First Step in the Translation of Alloy to Coq. ICFEM Salwa Souaf, Frédéric Loulergue
2019	—	`conf`	Automatic Optimization of Python Skeletal Parallel Programs. ICA3PP (1) Frédéric Loulergue, Jolan Philippe
2019	Misc	`conf`	Logic against ghosts: comparison of two proof approaches for a list module. SAC Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2019	C	`conf`	New List Skeletons for the Python Skeleton Library. PDCAT Frédéric Loulergue, Jolan Philippe
2019	Misc	`conf`	Parallel programming with Coq: map and reduce skeletons on trees. SAC Jolan Philippe, Frédéric Loulergue
2019	—	`conf`	PySke: Algorithmic Skeletons for Python. HPCS Jolan Philippe, Frédéric Loulergue
2019	—	`conf`	Towards Automatically Optimizing PySke Programs. HPCS Jolan Philippe, Frédéric Loulergue
2019	—	`conf`	Towards Full Proof Automation in Frama-C Using Auto-active Verification. NFM Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
2018	—	`ed.`	2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovation, SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI 2018, Guangzhou, China, October 8-12, 2018 SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI Guojun Wang, Qi Han, Md. Zakirul Alam Bhuiyan, Xiaoxing Ma, Frédéric Loulergue, Peng Li, Manuel Roveri, Lei Chen
2018	—	`conf`	A Cloud Brokerage Solution: Formal Methods Meet Security in Cloud Federations. HPCS Salwa Souaf, Pascal Berthomé, Frédéric Loulergue
2018	—	`conf`	A Lesson on Verification of IoT Software with Frama-C. HPCS Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2018	—	`conf`	Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. NFM Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2018	—	`conf`	Ghosts for Lists: From Axiomatic to Executable Specifications. TAP@STAF Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov
2018	—	`conf`	Interactive Bulk Synchronous Parallel Functional Programming in a Browser. SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI Julien Tesson, Frédéric Loulergue
2018	J	`jnl`	MMFilter : A CHR-Based Solver for Generation of Executions under Weak Memory Models. Comput. Lang. Syst. Struct. Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2018	—	`conf`	Parallel Programming with OCaml: A Tutorial. HPCS Victor Allombert, Mathias Bourgoin, Frédéric Loulergue
2018	—	`conf`	Strong Security Guarantees: From Alloy to Coq (Research Poster). HPCS Salwa Souaf, Frédéric Loulergue
2018	—	`conf`	Towards the Generation of Correct Java Programs (Research Poster). HPCS Jolan Philippe, Frédéric Loulergue
2018	—	`conf`	Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C. SecDev Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2018	—	`conf`	Verified Programs for Frequent Itemset Mining. SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI Frédéric Loulergue, Christopher D. Whitney
2017	J	`jnl`	A BSPlib-style API for Bulk Synchronous Parallel ML. Scalable Comput. Pract. Exp. Frédéric Loulergue
2017	C	`conf`	A Java Framework for High Level Parallel Programming Using Powerlists. PDCAT Virginia Niculescu, Frédéric Loulergue, Darius Bufnea, Adrian Sterca
2017	—	`conf`	A Verified Accumulate Algorithmic Skeleton. CANDAR Frédéric Loulergue
2017	J	`jnl`	Automated Generation of BSP Automata. Parallel Process. Lett. Thibaut Tachon, Chong Li, Gaétan Hains, Frédéric Loulergue
2017	J	`jnl`	Calculating Parallel Programs in Coq Using List Homomorphisms. Int. J. Parallel Program. Frédéric Loulergue, Wadoud Bousdira, Julien Tesson
2017	—	`conf`	Formalization of a Big Graph API in Coq. HPCS Jolan Philippe, Wadoud Bousdira, Frédéric Loulergue
2017	—	`conf`	From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation. VPT@ETAPS Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
2017	Misc	`conf`	Imperative BSPlib-style Communications in BSML. ICCS Frédéric Loulergue
2017	C	`conf`	Implementing Algorithmic Skeletons with Bulk Synchronous Parallel ML. PDCAT Frédéric Loulergue
2017	J	`jnl`	Introduction to the Special Issue on Practical Aspects of High-Level Parallel Programming. Scalable Comput. Pract. Exp. Frédéric Loulergue
2017	Misc	`conf`	Replicated Synchronization for Imperative BSP Programs. ICCS Arvid Jakobsson, Frédéric Dabrowski, Wadoud Bousdira, Frédéric Loulergue, Gaétan Hains
2017	—	`conf`	Towards a Verified Parallel Implementation of Frequent Itemset Mining. HPCS Christopher D. Whitney, Frédéric Loulergue
2016	—	`conf`	A CHR-Based Solver for Weak Memory Behaviors. CSTVA@ISSTA Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2016	C	`conf`	Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs. SCAM Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
2015	C	`conf`	A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C. FMICS Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
2015	J	`jnl`	A formal semantics of nested atomic sections with thread escape. Comput. Lang. Syst. Struct. Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard
2015	C	`conf`	Cloud Resources Placement based on Functional and Non-functional Requirements. SECRYPT Asma Guesmi, Patrice Clemente, Frédéric Loulergue, Pascal Berthomé
2015	Misc	`conf`	Nested atomic sections with thread escape: compilation. SAC Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard
2014	B	`conf`	A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. ITP Kento Emoto, Frédéric Loulergue, Julien Tesson
2014	—	`conf`	Development effort and performance trade-off in high-level parallel programming. HPCS Joeffrey Legaux, Frédéric Loulergue, Sylvain Jubertie
2014	Misc	`conf`	Formal derivation and extraction of a parallel program for the all nearest smaller values problem. SAC Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Legaux, Zhenjiang Hu
2014	Misc	`conf`	Handling Data-skew Effects in Join Operations Using MapReduce. ICCS Mohamad Al Hajj Hassan, Mostafa Bamha, Frédéric Loulergue
2014	Misc	`conf`	Implementing Powerlists with Bulk Synchronous Parallel ML. SYNASC Frédéric Loulergue, Virginia Niculescu, Julien Tesson
2014	Misc	`conf`	Nested atomic sections with thread escape: a formal definition. SAC Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard
2013	—	`conf`	Managing arbitrary distributions of arrays in Orléans Skeleton Library. HPCS Joeffrey Legaux, Frédéric Loulergue, Sylvain Jubertie
2013	C	`conf`	Nested Atomic Sections with Thread Escape: An Operational Semantics. PDCAT Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard
2013	Misc	`conf`	OSL: An Algorithmic Skeleton Library with Exceptions. ICCS Joeffrey Legaux, Frédéric Loulergue, Sylvain Jubertie
2013	—	`conf`	Powerlists in Coq: Programming and Reasoning. CANDAR Frédéric Loulergue, Virginia Niculescu, Simon Robillard
2013	—	`conf`	Programming with BSP Homomorphisms. Euro-Par Joeffrey Legaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, Julien Tesson
2012	—	`conf`	A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays. ICA3PP (1) Wadoud Bousdira, Frédéric Loulergue, Julien Tesson
2012	—	`conf`	Experiments in Parallel Matrix Multiplication on Multi-core Systems. ICA3PP (1) Joeffrey Legaux, Sylvain Jubertie, Frédéric Loulergue
2012	—	`conf`	Towards verified cloud computing environments. HPCS Frédéric Loulergue, Frédéric Gava, Nikolai Kosmatov, Matthieu Lemerre
2011	B	`conf`	A Formal Programming Model of Orléans Skeleton Library. PaCT Noman Javed, Frédéric Loulergue
2011	Misc	`conf`	AVerified Bulk Synchronous ParallelMLHeat Diffusion Simulation. ICCS Julien Tesson, Frédéric Loulergue
2011	—	`conf`	Parallel programming and performance predictability with Orléans Skeleton Library. HPCS Noman Javed, Frédéric Loulergue
2011	—	`conf`	Verification of a Heat Diffusion Simulation Written with Orléans Skeleton Library. PPAM (2) Noman Javed, Frédéric Loulergue
2010	J	`jnl`	Bulk synchronous parallel ML with exceptions. Future Gener. Comput. Syst. Louis Gesbert, Frédéric Gava, Frédéric Loulergue, Frédéric Dabrowski
2010	Misc	`conf`	Functional Parallel Programming with Revised Bulk Synchronous Parallel ML. ICNC Wadoud Bousdira, Frédéric Gava, Louis Gesbert, Frédéric Loulergue, Guillaume Petiot
2010	—	`conf`	Program Calculation in Coq. AMAST Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, Masato Takeichi
2010	C	`conf`	Systematic Development of Correct Bulk Synchronous Parallel Programs. PDCAT Louis Gesbert, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, Julien Tesson
2009	—	`conf`	OSL: Optimized Bulk Synchronous Parallel Skeletons on Distributed Arrays. APPT Noman Javed, Frédéric Loulergue
2007	Misc	`conf`	Divide-and-Conquer Parallel Programming with Minimally Synchronous Parallel ML. PPAM Radia Benheddi, Frédéric Loulergue
2007	Misc	`conf`	Formal Semantics of DRMA-Style Programming in BSPlib. PPAM Julien Tesson, Frédéric Loulergue
2007	J	`jnl`	Introduction to the special issue on semantics and costs models for high-level parallel programming. Comput. Lang. Syst. Struct. Frédéric Loulergue
2007	J	`jnl`	Practical Aspects of High-Level Parallel Programming. Scalable Comput. Pract. Exp. Anne Benoit, Frédéric Loulergue
2007	C	`conf`	Semantics of an Exception Mechanism for Bulk Synchronous Parallel ML. PDCAT Louis Gesbert, Frédéric Loulergue
2006	A	`conf`	A calculus of functional BSP programs with projection. IPDPS Frédéric Loulergue
2006	Misc	`conf`	Bulk Synchronous Parallel ML: Semantics and Implementation of the Parallel Juxtaposition. CSR Frédéric Loulergue, Radia Benheddi, Frédéric Gava, D. Louis-Régis
2006	J	`jnl`	Practical Aspects of High-Level Parallel Programming. Scalable Comput. Pract. Exp. Frédéric Loulergue
2005	J	`jnl`	A Functional Language for Departmental Metacomputing. Parallel Process. Lett. Frédéric Gava, Frédéric Loulergue
2005	J	`jnl`	A static analysis for Bulk Synchronous Parallel ML to avoid parallel nesting. Future Gener. Comput. Syst. Frédéric Gava, Frédéric Loulergue
2005	Misc	`conf`	Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction. International Conference on Computational Science (2) Frédéric Loulergue, Frédéric Gava, David Billiet
2005	C	`conf`	Optimizing Bulk Synchronous Parallel ML. SNPD Frédéric Loulergue
2005	J	`jnl`	Practical Aspects of High-Level Parallel Programming. Scalable Comput. Pract. Exp. Frédéric Loulergue
2005	J	`jnl`	Review of "Term Rewriting Systems by Terese", Cambridge University Press 2003, 0-521-39115-6. SIGACT News Frédéric Loulergue
2004	Misc	`conf`	Communication Primitives for Minimally Synchronous Parallel ML. International Conference on Computational Science Frédéric Loulergue
2004	J	`jnl`	Développement d'applications avec Objective CAML by E. Chailloux, P. Manoury and B. Pagano, O'Reilley, 2003. J. Funct. Program. Frédéric Loulergue
2004	—	`conf`	Management of Communication Environments for Minimally Synchronous Parallel ML. DAPSYS Frédéric Loulergue
2003	—	`conf`	A Calculus of Functional BSP Programs with Explicit Substitutions. PARCO Frédéric Loulergue
2003	C	`conf`	A Parallel Categorical Abstract Machine for Bulk Synchronous Parallel ML. SNPD Frédéric Gava, Frédéric Loulergue, Frédéric Dabrowski
2003	Misc	`conf`	A Parallel Virtual Machine for Bulk Synchronous Parallel ML. International Conference on Computational Science Frédéric Gava, Frédéric Loulergue
2003	B	`conf`	A Polymorphic Type System for Bulk Synchronous Parallel ML. PaCT Frédéric Gava, Frédéric Loulergue
2003	—	`conf`	A Rewriting Semantics for an Event-Oriented Functional Parallel Language. PARCO Frédéric Loulergue
2003	—	`conf`	Functional Bulk Synchronous Parallel Programming in C++. Applied Informatics Frédéric Dabrowski, Frédéric Loulergue
2003	—	`conf`	Parallel Juxtaposition for Bulk Synchronous Parllel ML. Euro-Par Frédéric Loulergue
2003	Misc	`conf`	Parallel Superposition for Bulk Synchronous Parallel ML. International Conference on Computational Science Frédéric Loulergue
2003	C	`conf`	Pattern Matching of Parallel Values in Bulk Synchronous Parallel ML. SNPD Frédéric Gava, Frédéric Loulergue, Frédéric Dabrowski
2003	J	`jnl`	Preface: Special Issue on High-Level Parallel Programming and Applications. Parallel Process. Lett. Gaétan Hains, Frédéric Loulergue
2003	C	`conf`	Semantics of Minimally Synchronous Parallel ML. SNPD Myrto Arapinis, Frédéric Loulergue, Frédéric Gava, Frédéric Dabrowski
2003	—	`conf`	Semantics of a Functional BSP Language with Imperative Features. PARCO Frédéric Gava, Frédéric Loulergue
2003	—	`conf`	Synthèse de types pour Bulk Synchronous Parallel ML. JFLA Frédéric Gava, Frédéric Loulergue
2002	—	`conf`	Implementation of a Functional Bulk Synchronous Parallel Programming Library. IASTED PDCS Frédéric Loulergue
2001	J	`jnl`	Concrete data structures and functional parallel programming. Theor. Comput. Sci. Gaétan Hains, Frédéric Loulergue, John Mullins
2001	J	`jnl`	Distributed Evaluation of Functional BSP Programs. Parallel Process. Lett. Frédéric Loulergue
2000	J	`jnl`	A calculus of functional BSP programs. Sci. Comput. Program. Frédéric Loulergue, Gaétan Hains, Christian Foisy
2000	—	`conf`	BSlambda ISHPC Frédéric Loulergue
2000	—	`conf`	Parallel composition and bulk synchronous parallel functional programming. Scottish Functional Programming Workshop Frédéric Loulergue
1999	—	`conf`	High Level BSP Programming: BSML and BSlambda. Scottish Functional Programming Workshop Olivier Ballereau, Frédéric Loulergue, Gaétan Hains
1997	—	`conf`	Functional Parallel Programming with Explicit Processes: Beyond SPMD. Euro-Par Frédéric Loulergue, Gaétan Hains