Tue 18 Jul 2023 11:10 - 11:35 at Anderson Seminar Room (Gates 271) - Verification

SyDPaCC (Systematic Development of programs for Parallel and Cloud Computing) is a framework for the Coq interactive theorem prover. It allows to systematically develop correct parallel programs from specifications via verified and automated program transformations. The obtained programs are scalable, i.e. able to run on numerous processors. SyDPaCC produces programs written in the multi-paradigm and functional programming language OCaml with calls to the BSML (Bulk Synchronous parallel ML) parallel programming library. In this paper we present ongoing work towards an extension of SyDPaCC to be able to produce Scala programs using Apache Spark for parallel processing.

Tue 18 Jul

Displayed time zone: Pacific Time (US & Canada) change

10:30 - 12:00
10:30
25m
Talk
Verifying C++ dynamic binding
FTfJP
Niels Mommen KU Leuven, Bart Jacobs imec-DistriNet, Dept. CS, KU Leuven
Link to publication DOI Pre-print
10:55
15m
Talk
Correctness-by-Construction meets Refinement Types
FTfJP
Baber Rehman University of Hong Kong
11:10
25m
Talk
Towards Verified Scalable Parallel Computing with Coq and Spark
FTfJP
Frederic Loulergue Université d'Orléans, Jolan Philippe IMT Atlantique
DOI
11:35
25m
Talk
Constructing Structured SSA from FJ
FTfJP
Kenny Zhuo Ming Lu ISTD, Singapore University of Technology and Design, Daniel Yu Hian Low Singapore University of Technology and Design