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 proceedingConference Article in proceedingAcademicpeer-review


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 languageEnglish
Title of host publicationFormal Methods
Subtitle of host publication25th International Symposium, FM 2023, Proceedings
EditorsMarsha Chechik, Joost-Pieter Katoen, Martin Leucker
PublisherSpringer, Cham
Number of pages19
ISBN (Electronic)978-3-031-27481-7
ISBN (Print)9783031274800
Publication statusPublished - Mar 2023
Event25th International Symposium on Formal Methods - Lübeck, Germany
Duration: 6 Mar 202310 Mar 2023
Conference number: 25

Publication series

SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14000 LNCS


Conference25th International Symposium on Formal Methods
Abbreviated titleFM 2023


Dive into the research topics of 'VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs'. Together they form a unique fingerprint.

Cite this