VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs

Petra van den Bos; Sung-Shik Jongmans

doi:10.1007/978-3-031-27481-7_19

VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs

Petra van den Bos, Sung-Shik Jongmans

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

40 Downloads (Pure)

Abstract

We present VeyMont: a deductive verification tool that aims to make reasoning about functional correctness and deadlock freedom of parallel programs (relatively complex) as easy as that of sequential programs (relatively simple). The novelty of VeyMont is that it ``inverts the workflow'': it supports a new method to parallelise verified programs, in contrast to existing methods to verify parallel programs. Inspired by methods for distributed systems, VeyMont targets coarse-grained parallelism among threads (i.e., whole-program parallelisation) instead of fine-grained parallelism among tasks (e.g., loop parallelisation).

Original language	English
Title of host publication	Formal Methods
Subtitle of host publication	25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings
Editors	Marsha Chechik, Joost-Pieter Katoen, Martin Leucker
Place of Publication	Cham
Publisher	Springer Nature
Pages	321-339
Number of pages	19
ISBN (Electronic)	978-3-031-27481-7
ISBN (Print)	978-3-031-27480-0
DOIs	https://doi.org/10.1007/978-3-031-27481-7_19
Publication status	Published - 3 Mar 2023
Event	25th International Symposium on Formal Methods, FM 2023 - Lübeck, Germany Duration: 6 Mar 2023 → 10 Mar 2023 Conference number: 25

Publication series

Name	Lecture Notes in Computer Science
Volume	14000

Conference

Conference	25th International Symposium on Formal Methods, FM 2023
Abbreviated title	FM
Country/Territory	Germany
City	Lübeck
Period	6/03/23 → 10/03/23

Keywords

2023 OA procedure

Access to Document

10.1007/978-3-031-27481-7_19

978-3-031-27481-7_19Final published version, 1.68 MBLicence: Taverne

Cite this

van den Bos, P., & Jongmans, S.-S. (2023). VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs. In M. Chechik, J.-P. Katoen, & M. Leucker (Eds.), Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings (pp. 321-339). (Lecture Notes in Computer Science; Vol. 14000). Springer Nature. https://doi.org/10.1007/978-3-031-27481-7_19

van den Bos, Petra ; Jongmans, Sung-Shik. / VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs. Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings. editor / Marsha Chechik ; Joost-Pieter Katoen ; Martin Leucker. Cham : Springer Nature, 2023. pp. 321-339 (Lecture Notes in Computer Science).

@inproceedings{a86b0d9582a442d1ad6b93477bce3747,

title = "VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs",

abstract = "We present VeyMont: a deductive verification tool that aims to make reasoning about functional correctness and deadlock freedom of parallel programs (relatively complex) as easy as that of sequential programs (relatively simple). The novelty of VeyMont is that it ``inverts the workflow'': it supports a new method to parallelise verified programs, in contrast to existing methods to verify parallel programs. Inspired by methods for distributed systems, VeyMont targets coarse-grained parallelism among threads (i.e., whole-program parallelisation) instead of fine-grained parallelism among tasks (e.g., loop parallelisation).",

keywords = "2023 OA procedure",

author = "{van den Bos}, Petra and Sung-Shik Jongmans",

year = "2023",

month = mar,

day = "3",

doi = "10.1007/978-3-031-27481-7_19",

language = "English",

isbn = "978-3-031-27480-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer Nature",

pages = "321--339",

editor = "Marsha Chechik and Joost-Pieter Katoen and Martin Leucker",

booktitle = "Formal Methods",

address = "Switzerland",

note = "25th International Symposium on Formal Methods, FM 2023, FM ; Conference date: 06-03-2023 Through 10-03-2023",

}

van den Bos, P & Jongmans, S-S 2023, VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs. in M Chechik, J-P Katoen & M Leucker (eds), Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14000, Springer Nature, Cham, pp. 321-339, 25th International Symposium on Formal Methods, FM 2023, Lübeck, Schleswig-Holstein, Germany, 6/03/23. https://doi.org/10.1007/978-3-031-27481-7_19

VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs. / van den Bos, Petra; Jongmans, Sung-Shik.
Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings. ed. / Marsha Chechik; Joost-Pieter Katoen; Martin Leucker. Cham: Springer Nature, 2023. p. 321-339 (Lecture Notes in Computer Science; Vol. 14000).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs

AU - van den Bos, Petra

AU - Jongmans, Sung-Shik

N1 - Conference code: 25

PY - 2023/3/3

Y1 - 2023/3/3

N2 - We present VeyMont: a deductive verification tool that aims to make reasoning about functional correctness and deadlock freedom of parallel programs (relatively complex) as easy as that of sequential programs (relatively simple). The novelty of VeyMont is that it ``inverts the workflow'': it supports a new method to parallelise verified programs, in contrast to existing methods to verify parallel programs. Inspired by methods for distributed systems, VeyMont targets coarse-grained parallelism among threads (i.e., whole-program parallelisation) instead of fine-grained parallelism among tasks (e.g., loop parallelisation).

AB - We present VeyMont: a deductive verification tool that aims to make reasoning about functional correctness and deadlock freedom of parallel programs (relatively complex) as easy as that of sequential programs (relatively simple). The novelty of VeyMont is that it ``inverts the workflow'': it supports a new method to parallelise verified programs, in contrast to existing methods to verify parallel programs. Inspired by methods for distributed systems, VeyMont targets coarse-grained parallelism among threads (i.e., whole-program parallelisation) instead of fine-grained parallelism among tasks (e.g., loop parallelisation).

KW - 2023 OA procedure

U2 - 10.1007/978-3-031-27481-7_19

DO - 10.1007/978-3-031-27481-7_19

M3 - Conference contribution

SN - 978-3-031-27480-0

T3 - Lecture Notes in Computer Science

SP - 321

EP - 339

BT - Formal Methods

A2 - Chechik, Marsha

A2 - Katoen, Joost-Pieter

A2 - Leucker, Martin

PB - Springer Nature

CY - Cham

T2 - 25th International Symposium on Formal Methods, FM 2023

Y2 - 6 March 2023 through 10 March 2023

ER -

van den Bos P, Jongmans SS. VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs. In Chechik M, Katoen JP, Leucker M, editors, Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings. Cham: Springer Nature. 2023. p. 321-339. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-27481-7_19