Frédéric Loulergue

Heike Wehrheim

Formal Aspects Comput., March, 2024

Component-based Distributed Software Reconfiguration:A Verification-oriented Survey.

[BibT_eX]

[DOI]

ACM Comput. Surv., January, 2024

Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 18th International Conference, 2024

SyDPaCC: A Framework for the Development of Verified Scalable Parallel Functional Programs.

[BibT_eX]

[DOI]

Jordan Ischard

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification, 2024

Combining Deductive Verification with Shape Analysis.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2024

2023

Guest Editor's Note: High-Level Parallel Programming 2021.

[BibT_eX]

[DOI]

Int. J. Parallel Program., October, 2023

Verified High Performance Computing: The SyDPaCC Approach.

[BibT_eX]

[DOI]

Ali Ed-Dbali

Proceedings of the Verification and Evaluation of Computer and Communication Systems, 2023

Verified Scalable Parallel Computing with Why3.

[BibT_eX]

[DOI]

Olivia Proust

Proceedings of the Software Engineering and Formal Methods - 21st International Conference, 2023

Towards Formal Verification of a TPM Software Stack.

[BibT_eX]

[DOI]

Proceedings of the iFM 2023 - 18th International Conference, 2023

Towards Verified Scalable Parallel Computing with Coq and Spark.

[BibT_eX]

[DOI]

Proceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs, 2023

2021

Experience Report: Teaching Code Analysis and Verification Using Frama-C.

[BibT_eX]

[DOI]

Proceedings of the Proceedings First Workshop on Applicable Formal Methods, 2021

2020

Transforming powerlist-based divide-and-conquer programs for an improved execution model.

[BibT_eX]

[DOI]

J. Supercomput., 2020

Preface to the special issue on Formal Approaches to Parallel and Distributed Systems 2018.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2020

Verified Runtime Assertion Checking for Memory Properties.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 14th International Conference, 2020

Reflections on the Design of Parallel Programming Frameworks.

[BibT_eX]

[DOI]

Adrian Sterca

Proceedings of the Evaluation of Novel Approaches to Software Engineering, 2020

Pattern-driven Design of a Multiparadigm Parallel Programming Framework.

[BibT_eX]

[DOI]

Proceedings of the 15th International Conference on Evaluation of Novel Approaches to Software Engineering, 2020

2019

Parallel programming with Coq: map and reduce skeletons on trees.

[BibT_eX]

[DOI]

Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, 2019

Logic against ghosts: comparison of two proof approaches for a list module.

[BibT_eX]

[DOI]

Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, 2019

New List Skeletons for the Python Skeleton Library.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Parallel and Distributed Computing, 2019

Towards Full Proof Automation in Frama-C Using Auto-active Verification.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

Towards Automatically Optimizing PySke Programs.

[BibT_eX]

[DOI]

Proceedings of the 17th International Conference on High Performance Computing & Simulation, 2019

PySke: Algorithmic Skeletons for Python.

[BibT_eX]

[DOI]

Proceedings of the 17th International Conference on High Performance Computing & Simulation, 2019

A First Step in the Translation of Alloy to Coq.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2019

Automatic Optimization of Python Skeletal Parallel Programs.

[BibT_eX]

[DOI]

Proceedings of the Algorithms and Architectures for Parallel Processing, 2019

2018

MMFilter : A CHR-Based Solver for Generation of Executions under Weak Memory Models.

[BibT_eX]

[DOI]

Comput. Lang. Syst. Struct., 2018

Interactive Bulk Synchronous Parallel Functional Programming in a Browser.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE SmartWorld, 2018

Verified Programs for Frequent Itemset Mining.

[BibT_eX]

[DOI]

Christopher D. Whitney

Proceedings of the 2018 IEEE SmartWorld, 2018

Ghosts for Lists: From Axiomatic to Executable Specifications.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 12th International Conference, 2018

Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE Cybersecurity Development, SecDev 2018, Cambridge, MA, USA, 2018

Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 10th International Symposium, 2018

Strong Security Guarantees: From Alloy to Coq (Research Poster).

[BibT_eX]

[DOI]

Proceedings of the 2018 International Conference on High Performance Computing & Simulation, 2018

A Cloud Brokerage Solution: Formal Methods Meet Security in Cloud Federations.

[BibT_eX]

[DOI]

Pascal Berthomé

Proceedings of the 2018 International Conference on High Performance Computing & Simulation, 2018

Towards the Generation of Correct Java Programs (Research Poster).

[BibT_eX]

[DOI]

Proceedings of the 2018 International Conference on High Performance Computing & Simulation, 2018

A Lesson on Verification of IoT Software with Frama-C.

[BibT_eX]

[DOI]

Proceedings of the 2018 International Conference on High Performance Computing & Simulation, 2018

Parallel Programming with OCaml: A Tutorial.

[BibT_eX]

[DOI]

Victor Allombert

Mathias Bourgoin

Proceedings of the 2018 International Conference on High Performance Computing & Simulation, 2018

2017

A BSPlib-style API for Bulk Synchronous Parallel ML.

[BibT_eX]

[DOI]

Scalable Comput. Pract. Exp., 2017

Introduction to the Special Issue on Practical Aspects of High-Level Parallel Programming.

[BibT_eX]

[DOI]

Scalable Comput. Pract. Exp., 2017

Automated Generation of BSP Automata.

[BibT_eX]

[DOI]

Parallel Process. Lett., 2017

Calculating Parallel Programs in Coq Using List Homomorphisms.

[BibT_eX]

[DOI]

Wadoud Bousdira

Int. J. Parallel Program., 2017

From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fifth International Workshop on Verification and Program Transformation, 2017

A Java Framework for High Level Parallel Programming Using Powerlists.

[BibT_eX]

[DOI]

Proceedings of the 18th International Conference on Parallel and Distributed Computing, 2017

Implementing Algorithmic Skeletons with Bulk Synchronous Parallel ML.

[BibT_eX]

[DOI]

Proceedings of the 18th International Conference on Parallel and Distributed Computing, 2017

Towards a Verified Parallel Implementation of Frequent Itemset Mining.

[BibT_eX]

[DOI]

Christopher D. Whitney

Proceedings of the 2017 International Conference on High Performance Computing & Simulation, 2017

Formalization of a Big Graph API in Coq.

[BibT_eX]

[DOI]

Wadoud Bousdira

Proceedings of the 2017 International Conference on High Performance Computing & Simulation, 2017

Imperative BSPlib-style Communications in BSML.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Computational Science, 2017

Replicated Synchronization for Imperative BSP Programs.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Computational Science, 2017

A Verified Accumulate Algorithmic Skeleton.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Symposium on Computing and Networking, 2017

2016

Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Working Conference on Source Code Analysis and Manipulation, 2016

A CHR-Based Solver for Weak Memory Behaviors.

[BibT_eX]

[DOI]

Proceedings of the 7th Workshop on Constraint Solvers in Testing, 2016

2015

A formal semantics of nested atomic sections with thread escape.

[BibT_eX]

[DOI]

Comput. Lang. Syst. Struct., 2015

Cloud Resources Placement based on Functional and Non-functional Requirements.

[BibT_eX]

[DOI]

Proceedings of the SECRYPT 2015, 2015

Nested atomic sections with thread escape: compilation.

[BibT_eX]

[DOI]

Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015

A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2015

2014

Implementing Powerlists with Bulk Synchronous Parallel ML.

[BibT_eX]

[DOI]

Proceedings of the 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2014

Formal derivation and extraction of a parallel program for the all nearest smaller values problem.

[BibT_eX]

[DOI]

Proceedings of the Symposium on Applied Computing, 2014

Nested atomic sections with thread escape: a formal definition.

[BibT_eX]

[DOI]

Proceedings of the Symposium on Applied Computing, 2014

A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction.

[BibT_eX]

[DOI]

Kento Emoto

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Handling Data-skew Effects in Join Operations Using MapReduce.

[BibT_eX]

[DOI]

Mohamad Al Hajj Hassan

Mostafa Bamha

Proceedings of the International Conference on Computational Science, 2014

Development effort and performance trade-off in high-level parallel programming.

[BibT_eX]

[DOI]

Proceedings of the International Conference on High Performance Computing & Simulation, 2014

2013

Nested Atomic Sections with Thread Escape: An Operational Semantics.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Parallel and Distributed Computing, 2013

Managing arbitrary distributions of arrays in Orléans Skeleton Library.

[BibT_eX]

[DOI]

Proceedings of the International Conference on High Performance Computing & Simulation, 2013

OSL: An Algorithmic Skeleton Library with Exceptions.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Computational Science, 2013

Powerlists in Coq: Programming and Reasoning.

[BibT_eX]

[DOI]

Simon Robillard

Proceedings of the First International Symposium on Computing and Networking, 2013

Programming with BSP Homomorphisms.

[BibT_eX]

[DOI]

Proceedings of the Euro-Par 2013 Parallel Processing, 2013

2012

Towards verified cloud computing environments.

[BibT_eX]

[DOI]

Proceedings of the 2012 International Conference on High Performance Computing & Simulation, 2012

Experiments in Parallel Matrix Multiplication on Multi-core Systems.

[BibT_eX]

[DOI]

Proceedings of the Algorithms and Architectures for Parallel Processing, 2012

A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays.

[BibT_eX]

[DOI]

Wadoud Bousdira

Proceedings of the Algorithms and Architectures for Parallel Processing, 2012

2011

AVerified Bulk Synchronous ParallelMLHeat Diffusion Simulation.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Computational Science, 2011

Verification of a Heat Diffusion Simulation Written with Orléans Skeleton Library.

[BibT_eX]

[DOI]

Proceedings of the Parallel Processing and Applied Mathematics, 2011

A Formal Programming Model of Orléans Skeleton Library.

[BibT_eX]

[DOI]

Proceedings of the Parallel Computing Technologies - 11th International Conference, 2011

Parallel programming and performance predictability with Orléans Skeleton Library.

[BibT_eX]

[DOI]

Proceedings of the 2011 International Conference on High Performance Computing & Simulation, 2011

2010

Bulk synchronous parallel ML with exceptions.

[BibT_eX]

[DOI]

Future Gener. Comput. Syst., 2010

Systematic Development of Correct Bulk Synchronous Parallel Programs.

[BibT_eX]

[DOI]

Proceedings of the 2010 International Conference on Parallel and Distributed Computing, 2010

Functional Parallel Programming with Revised Bulk Synchronous Parallel ML.

[BibT_eX]

[DOI]

Proceedings of the First International Conference on Networking and Computing, 2010

Program Calculation in Coq.

[BibT_eX]

[DOI]

Proceedings of the Algebraic Methodology and Software Technology, 2010

2009

OSL: Optimized Bulk Synchronous Parallel Skeletons on Distributed Arrays.

[BibT_eX]

[DOI]

Proceedings of the Advanced Parallel Processing Technologies, 8th International Symposium, 2009

2007

Practical Aspects of High-Level Parallel Programming.

[BibT_eX]

[DOI]

Anne Benoit

Scalable Comput. Pract. Exp., 2007

Introduction to the special issue on semantics and costs models for high-level parallel programming.

[BibT_eX]

[DOI]

Comput. Lang. Syst. Struct., 2007

Formal Semantics of DRMA-Style Programming in BSPlib.

[BibT_eX]

[DOI]

Proceedings of the Parallel Processing and Applied Mathematics, 2007

Divide-and-Conquer Parallel Programming with Minimally Synchronous Parallel ML.

[BibT_eX]

[DOI]

Radia Benheddi

Proceedings of the Parallel Processing and Applied Mathematics, 2007

Semantics of an Exception Mechanism for Bulk Synchronous Parallel ML.

[BibT_eX]

[DOI]

Louis Gesbert

Proceedings of the Eighth International Conference on Parallel and Distributed Computing, 2007

2006

A calculus of functional BSP programs with projection.

[BibT_eX]

[DOI]

Proceedings of the 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), 2006

Bulk Synchronous Parallel ML: Semantics and Implementation of the Parallel Juxtaposition.

[BibT_eX]

[DOI]

Proceedings of the Computer Science, 2006

2005

Review of "Term Rewriting Systems by Terese", Cambridge University Press 2003, 0-521-39115-6.

[BibT_eX]

[DOI]

SIGACT News, 2005

Practical Aspects of High-Level Parallel Programming.

[BibT_eX]

[DOI]

Scalable Comput. Pract. Exp., 2005

A Functional Language for Departmental Metacomputing.

[BibT_eX]

[DOI]

Parallel Process. Lett., 2005

A static analysis for Bulk Synchronous Parallel ML to avoid parallel nesting.

[BibT_eX]

[DOI]

Future Gener. Comput. Syst., 2005

Optimizing Bulk Synchronous Parallel ML.

[BibT_eX]

[DOI]

Proceedings of the 6th ACIS International Conference on Software Engineering, 2005

Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction.

[BibT_eX]

[DOI]

David Billiet

Proceedings of the Computational Science, 2005

2004

Développement d'applications avec Objective CAML by E. Chailloux, P. Manoury and B. Pagano, O'Reilley, 2003.

[BibT_eX]

[DOI]

J. Funct. Program., 2004

Communication Primitives for Minimally Synchronous Parallel ML.

[BibT_eX]

[DOI]

Proceedings of the Computational Science, 2004

Management of Communication Environments for Minimally Synchronous Parallel ML.

[BibT_eX]

Proceedings of the Distributed and Parallel Systems: Cluster and Grid Computing (DAPSYS 2004, 2004

2003

Preface: Special Issue on High-Level Parallel Programming and Applications.

[BibT_eX]

[DOI]

Parallel Process. Lett., 2003

Pattern Matching of Parallel Values in Bulk Synchronous Parallel ML.

[BibT_eX]

Proceedings of the ACIS Fourth International Conference on Software Engineering, 2003

A Parallel Categorical Abstract Machine for Bulk Synchronous Parallel ML.

[BibT_eX]

Proceedings of the ACIS Fourth International Conference on Software Engineering, 2003

Semantics of Minimally Synchronous Parallel ML.

[BibT_eX]

Proceedings of the ACIS Fourth International Conference on Software Engineering, 2003

A Calculus of Functional BSP Programs with Explicit Substitutions.

[BibT_eX]

Proceedings of the Parallel Computing: Software Technology, 2003

A Rewriting Semantics for an Event-Oriented Functional Parallel Language.

[BibT_eX]

Proceedings of the Parallel Computing: Software Technology, 2003

Semantics of a Functional BSP Language with Imperative Features.

[BibT_eX]

Proceedings of the Parallel Computing: Software Technology, 2003

A Polymorphic Type System for Bulk Synchronous Parallel ML.

[BibT_eX]

[DOI]

Proceedings of the Parallel Computing Technologies, 2003

Synthèse de types pour Bulk Synchronous Parallel ML.

[BibT_eX]

Proceedings of the Journées francophones des langages applicatifs (JFLA'03), 2003

Parallel Superposition for Bulk Synchronous Parallel ML.

[BibT_eX]

[DOI]

Proceedings of the Computational Science - ICCS 2003, 2003

A Parallel Virtual Machine for Bulk Synchronous Parallel ML.

[BibT_eX]

[DOI]

Proceedings of the Computational Science - ICCS 2003, 2003

Parallel Juxtaposition for Bulk Synchronous Parllel ML.

[BibT_eX]

[DOI]

Proceedings of the Euro-Par 2003. Parallel Processing, 2003

Functional Bulk Synchronous Parallel Programming in C++.

[BibT_eX]

Proceedings of the 21st IASTED International Multi-Conference on Applied Informatics (AI 2003), 2003

2002

Implementation of a Functional Bulk Synchronous Parallel Programming Library.

[BibT_eX]

Proceedings of the International Conference on Parallel and Distributed Computing Systems, 2002

2001

Concrete data structures and functional parallel programming.

[BibT_eX]

[DOI]

John Mullins

Theor. Comput. Sci., 2001

Distributed Evaluation of Functional BSP Programs.

[BibT_eX]

[DOI]

Parallel Process. Lett., 2001

2000

A calculus of functional BSP programs.

[BibT_eX]

[DOI]

Christian Foisy

Sci. Comput. Program., 2000

Parallel composition and bulk synchronous parallel functional programming.

[BibT_eX]

Proceedings of the Selected papers from the 2nd Scottish Functional Programming Workshop (SFP00), 2000

BSlambda<sub><i>p</i></sub>: Functional BSP Programs on Enumerated Vectors.

[BibT_eX]

[DOI]

Proceedings of the High Performance Computing, Third International Symposium, 2000

1999

High Level BSP Programming: BSML and BSlambda.

[BibT_eX]

Olivier Ballereau

Proceedings of the Selected papers from the 1st Scottish Functional Programming Workshop (SFP99), 1999

1997

Functional Parallel Programming with Explicit Processes: Beyond SPMD.

[BibT_eX]

[DOI]