logo
科言猫学术研究的AI总结
language
手机端手机端
  • Phone Feature微信小程序
简体中文简体中文
notice消息通知
博客博客
delete
arrow
返回

Deductively verifying functional scalable parallel programs with Why3

delete2026-02-01
delete0
PRE
AI
F
Frédéric Loulergue *
O
Olivia Proust
DOI：10.1007/s10270-025-01340-ydelete
delete原文链接
delete原文求助
delete分享
delete收藏
摘要

摘要

En 中文
Bulk同步并行（BSP）是一种简单而现实的可扩展并行计算模型。BSML是用于多范式语言OCaml的纯函数库，体现了BSP的原则。我们提出使用WhyML（Why3的规范语言）对BSML原语进行形式化，并规范和证明构成标准库的一组并行函数的正确性。我们开发和验证了基于转换定理和一组列表上的顺序函数与算法骨架（即以并行方式实现并操作分布式列表的函数）对应关系的BSML应用程序的正确性。利用Why3从WhyML代码生成OCaml代码的功能，我们在并行机器上实验了这些应用程序。
Keyword:
Software engineering
Formal methods
Scalable parallel computing
Functional programming
Deductive verification
Why3

期刊

S
Software and Systems Modeling
IF:
3.2
论文数:
61
被引数:
1.9K

机构

U
universite de orleans
学者数:
3.6K
论文数: 2.7K
被引数: 1
引用论文

引用论文

New implementation of a BSP composition primitive with application to the implementation of algorithmic skeletons
err2009 IEEE International Symposium on Parallel & Distributed Processing
IF0
err2009-05-01
err0
PREAI
errGava,F.; Garnier,I.
err分享
err收藏
A denotational semantics of textually aligned SPMD programs
errJournal of Logical and Algebraic Methods in Programming
IF0
err2019-11-01
err0
PREAI
errDabrowski,Frédéric
err分享
err收藏
Formal derivation and extraction of a parallel program for the all nearest smaller values problem
errProceedings of the 29th Annual ACM Symposium on Applied Computing
IF0
err2014-03-24
err0
PREAI
errLoulergue,Frédéric; Robillard,Simon; Tesson,Julien; Legaux,Joeffrey; Hu,Zhenjiang
err分享
err收藏
Parallel Scientific Computation
err
IF0
err2020-10-22
err0
PREAI
errRob H. Bisseling
err分享
err收藏
Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation
errLecture Notes in Computer Science
IF0
err2024-01-01
err0
PREAI
errLermusiaux,Pierre; Montagu,Benoît
err分享
err收藏
Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications使用Coq进行Hadoop MapReduce应用的规范与程序提取
errLecture Notes in Computer Science
IF0
err2011-01-01
err0
PREAI
errKosuke Ono; Yoichi Hirai; Yoshinori Tanabe; Natsuko Noda; Masami Hagiya
err分享
err收藏
FORMAL PROOFS OF FUNCTIONAL BSP PROGRAMS
errParallel Processing Letters
IF0
err2003-09-01
err0
PREAI
errGAVA,FRÉDÉRIC
err分享
err收藏
A calculus of functional BSP programs
errScience of Computer Programming
IF0
err2000-05-01
err0
errOAAI
errFrédéric Loulergue; Gaétan Hains; Christian Foisy
err分享
err收藏
A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification
errLecture Notes in Computer Science
IF0
err2018-01-01
err0
PREAI
errGuéneau,Armaël; Charguéraud,Arthur; Pottier,François
err分享
err收藏
GOSPEL—Providing OCaml with a Formal Specification Language
errLecture Notes in Computer Science
IF0
err2019-01-01
err0
PREAI
errCharguéraud,Arthur; Filliâtre,Jean-Christophe; Lourenço,Cláudio; Pereira,Mário
err分享
err收藏
学者 查看更多内容