Skip to main content
Conference Proceedings

Verification of a heat diffusion simulation written with Orléans Skeleton Library

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2012) 7204 LNCS(PART 2) 91-100
DOI: 10.1007/978-3-642-31500-8_10
0Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Orléans Skeleton Library (OSL) provides a set of algorithmic skeletons as a C++ library on top of MPI. The parallel programming approach of OSL is a structured one, which eases the reasoning about the performance and correctness of the programs. In this paper we present the verification of a heat diffusion simulation program, written in OSL, using the Coq proof assistant. The specification used in proving the correctness is a discretisation of the heat equation. © 2012 Springer-Verlag.

Author supplied keywords

Cite

CITATION STYLE

APA

Javed, N., & Loulergue, F. (2012). Verification of a heat diffusion simulation written with Orléans Skeleton Library. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7204 LNCS, pp. 91–100). https://doi.org/10.1007/978-3-642-31500-8_10

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free