Verified scalable parallel computing with Why3

DOI10.1007/978-3-031-47115-5_14MaRDI QIDQ6550601zbMATH OpenFDO

Authors Olivia Proust, F. Loulergue

Publication date 5 June 2024

Full work available at URL https://doi.org/10.1007/978-3-031-47115-5_14

zbMATH Keywords

deductive verificationfunctional programminginteractive theorem provingscalable parallel computing

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2102059
• scientific article; zbMATH DE number 2009834
• A calculus of functional BSP programs
• Why3 -- where programs meet provers
• Axiomatization and characterization of BSP algorithms

Cites work

• A denotational semantics of textually aligned SPMD programs
• A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
• scientific article; zbMATH DE number 43723 (Why is no real title available?)

This page was built for publication: Verified scalable parallel computing with Why3

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6550601)