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

^*Corresponding author for this work

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

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, Proceedings
Editors	Marsha Chechik, Joost-Pieter Katoen, Martin Leucker
Publisher	Springer, Cham
Pages	321-339
Number of pages	19
Edition	1
ISBN (Electronic)	978-3-031-27481-7
ISBN (Print)	9783031274800
DOIs	https://doi.org/10.1007/978-3-031-27481-7_19
Publication status	Published - Mar 2023
Event	25th International Symposium on Formal Methods - Lübeck, Germany Duration: 6 Mar 2023 → 10 Mar 2023 Conference number: 25

Publication series

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14000 LNCS
ISSN	0302-9743

Conference

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

Access to Document

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

Cite this

van den Bos, Petra ; Jongmans, Sung Shik. / VeyMont : Parallelising Verified Programs Instead of Verifying Parallel Programs. Formal Methods: 25th International Symposium, FM 2023, Proceedings. editor / Marsha Chechik ; Joost-Pieter Katoen ; Martin Leucker. 1. ed. Springer, Cham, 2023. pp. 321-339 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14000 LNCS).

@inproceedings{b3b5296bb1b9472b95018ca2ef5f6d87,

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).",

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

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 25th International Symposium on Formal Methods, FM 2023 ; Conference date: 06-03-2023 Through 10-03-2023",

year = "2023",

month = mar,

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

language = "English",

isbn = "9783031274800",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer, Cham",

pages = "321--339",

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

booktitle = "Formal Methods",

edition = "1",

}

van den Bos, P & Jongmans, SS 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, Proceedings. 1 edn, Springer, Cham, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14000 LNCS, pp. 321-339, 25th International Symposium on Formal Methods, Lübeck, 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, Proceedings. ed. / Marsha Chechik; Joost-Pieter Katoen; Martin Leucker. 1. ed. Springer, Cham, 2023. p. 321-339 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14000 LNCS).

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

TY - GEN

T1 - VeyMont

T2 - 25th International Symposium on Formal Methods

AU - van den Bos, Petra

AU - Jongmans, Sung Shik

N1 - Conference code: 25

PY - 2023/3

Y1 - 2023/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).

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

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

M3 - Conference Article in proceeding

AN - SCOPUS:85151056934

SN - 9783031274800

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 321

EP - 339

BT - Formal Methods

A2 - Chechik, Marsha

A2 - Katoen, Joost-Pieter

A2 - Leucker, Martin

PB - Springer, Cham

Y2 - 6 March 2023 through 10 March 2023

ER -