Bridging the Implementation Gap: Advancements in Model-Based Concurrent Program Verification

Robert Rubbens

doi:10.3990/1.9789036569101

Bridging the Implementation Gap: Advancements in Model-Based Concurrent Program Verification

Robert Rubbens

Formal Methods and Tools

Research output: Thesis › PhD Thesis - Research UT, graduation UT

29 Downloads (Pure)

Abstract

This thesis considers the field of program correctness and verification, which strives to develop tools and techniques to find problems in software. That way, costly, lethal or global software catastrophes can be detected earlier.

We first consider how the deductive verifier VerCors can be applied to an industrial codebase. We find one suspected bug, confirm it with VerCors, and report what is needed to bring industry and program verification closer.

We then focus on integrating VerCors with a framework for rigorous software design, JavaBIP. This combination can help architecture designers ensure that the system implementation respects requirements that are otherwise left implicit and unchecked.

Next, choreographies are considered, a domain-specific language for designing distributed systems in a holistic manner. Previous work has introduced the choreographic verifier VeyMont, which verifies and generates code for choreographies. We extend VeyMont choreographies with support for shared memory, allowing more choreographies to be expressed and verified.

In the final part of this thesis, we extend VeyMont choreographies with support for parameterization. This means the number of participants in a choreography is defined by a run-time parameter. We introduce light constraints on the choreography language to keep verification and code generation tractable.

Original language	English
Qualification	Doctor of Philosophy
Awarding Institution	University of Twente
Supervisors/Advisors	Huisman, Marieke, Supervisor van den Bos, Petra, Co-Supervisor
Award date	15 Oct 2025
Place of Publication	Enschede
Publisher	University of Twente
Print ISBNs	978-90-365-6909-5
Electronic ISBNs	978-90-365-6910-1
DOIs	https://doi.org/10.3990/1.9789036569101
Publication status	Published - 15 Oct 2025

Keywords

formal methods
distributed systems
program verification
concurrency
choreographies

Access to Document

10.3990/1.9789036569101

thesis_R_RubbensFinal published version, 2.31 MB

Artefact of: Verified Parameterized Choreographies
Rubbens, R. (Creator), van den Bos, P. (Creator) & Huisman, M. (Creator), Zenodo, 20 Feb 2025
DOI: 10.5281/zenodo.14900264, https://zenodo.org/records/14900264 and 3 more links, https://doi.org/10.5281/zenodo.14900265, https://zenodo.org/records/14900265, https://zenodo.org/records/15223434 (show fewer)
Dataset
Artefact of: JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java
Rubbens, R. (Creator), Safina, L. (Creator), Huisman, M. (Creator), Bliudze, S. (Creator) & van den Bos, P. (Creator), 4TU.Centre for Research Data, 13 Mar 2024
DOI: 10.4121/21763274, https://data.4tu.nl/datasets/c24f1f76-19f3-456b-b6cd-087eef905e5d and one more link, https://data.4tu.nl/datasets/c24f1f76-19f3-456b-b6cd-087eef905e5d/1 (show fewer)
Dataset
Artifact of: VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory
Rubbens, R. (Creator), Huisman, M. (Creator) & van den Bos, P. (Creator), Zenodo, 20 Aug 2024
DOI: 10.5281/zenodo.13348213, https://zenodo.org/records/13348214 and 2 more links, https://doi.org/10.5281/zenodo.13348214, https://github.com/utwente-fmt/vercors (show fewer)
Dataset

2 Chapter
2 Conference contribution

Verified Parameterized Choreographies
Rubbens, R., van den Bos, P. & Huisman, M., 18 Jun 2025, Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings. Di Giusto, C. & Ravara, A. (eds.). Springer, p. 50-69 20 p. (Lecture Notes in Computer Science; vol. 15731 LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Open Access
File
VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory
Rubbens, R., van den Bos, P. V. & Huisman, M., 13 Nov 2024, Integrated Formal Methods - 19th International Conference, IFM 2024, Proceedings. Kosmatov, N. & Kovács, L. (eds.). Springer, p. 217-236 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 15234 LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Open Access
File
1 Citation (Scopus)

35 Downloads (Pure)
JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java
Bliudze, S., Bos, P. V. D., Huisman, M., Rubbens, R. & Safina, L., 20 Apr 2023, Fundamental Approaches to Software Engineering : 26th International Conference, FASE 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings. Lambers, L. & Uchitel, S. (eds.). p. 143-150 8 p.
Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

Open Access
File
2 Citations (Scopus)

147 Downloads (Pure)

Cite this

@phdthesis{a17300aed4e14c0090ceea54d6d56262,

title = "Bridging the Implementation Gap: Advancements in Model-Based Concurrent Program Verification",

abstract = "This thesis considers the field of program correctness and verification, which strives to develop tools and techniques to find problems in software. That way, costly, lethal or global software catastrophes can be detected earlier. We first consider how the deductive verifier VerCors can be applied to an industrial codebase. We find one suspected bug, confirm it with VerCors, and report what is needed to bring industry and program verification closer. We then focus on integrating VerCors with a framework for rigorous software design, JavaBIP. This combination can help architecture designers ensure that the system implementation respects requirements that are otherwise left implicit and unchecked. Next, choreographies are considered, a domain-specific language for designing distributed systems in a holistic manner. Previous work has introduced the choreographic verifier VeyMont, which verifies and generates code for choreographies. We extend VeyMont choreographies with support for shared memory, allowing more choreographies to be expressed and verified. In the final part of this thesis, we extend VeyMont choreographies with support for parameterization. This means the number of participants in a choreography is defined by a run-time parameter. We introduce light constraints on the choreography language to keep verification and code generation tractable.",

keywords = "formal methods, distributed systems, program verification, concurrency, choreographies",

author = "Robert Rubbens",

year = "2025",

month = oct,

day = "15",

doi = "10.3990/1.9789036569101",

language = "English",

isbn = "978-90-365-6909-5",

series = "IPA Dissertation Series",

publisher = "University of Twente",

number = "14",

address = "Netherlands",

type = "PhD Thesis - Research UT, graduation UT",

school = "University of Twente",

}

TY - THES

T1 - Bridging the Implementation Gap: Advancements in Model-Based Concurrent Program Verification

AU - Rubbens, Robert

PY - 2025/10/15

Y1 - 2025/10/15

N2 - This thesis considers the field of program correctness and verification, which strives to develop tools and techniques to find problems in software. That way, costly, lethal or global software catastrophes can be detected earlier. We first consider how the deductive verifier VerCors can be applied to an industrial codebase. We find one suspected bug, confirm it with VerCors, and report what is needed to bring industry and program verification closer. We then focus on integrating VerCors with a framework for rigorous software design, JavaBIP. This combination can help architecture designers ensure that the system implementation respects requirements that are otherwise left implicit and unchecked. Next, choreographies are considered, a domain-specific language for designing distributed systems in a holistic manner. Previous work has introduced the choreographic verifier VeyMont, which verifies and generates code for choreographies. We extend VeyMont choreographies with support for shared memory, allowing more choreographies to be expressed and verified. In the final part of this thesis, we extend VeyMont choreographies with support for parameterization. This means the number of participants in a choreography is defined by a run-time parameter. We introduce light constraints on the choreography language to keep verification and code generation tractable.

AB - This thesis considers the field of program correctness and verification, which strives to develop tools and techniques to find problems in software. That way, costly, lethal or global software catastrophes can be detected earlier. We first consider how the deductive verifier VerCors can be applied to an industrial codebase. We find one suspected bug, confirm it with VerCors, and report what is needed to bring industry and program verification closer. We then focus on integrating VerCors with a framework for rigorous software design, JavaBIP. This combination can help architecture designers ensure that the system implementation respects requirements that are otherwise left implicit and unchecked. Next, choreographies are considered, a domain-specific language for designing distributed systems in a holistic manner. Previous work has introduced the choreographic verifier VeyMont, which verifies and generates code for choreographies. We extend VeyMont choreographies with support for shared memory, allowing more choreographies to be expressed and verified. In the final part of this thesis, we extend VeyMont choreographies with support for parameterization. This means the number of participants in a choreography is defined by a run-time parameter. We introduce light constraints on the choreography language to keep verification and code generation tractable.

KW - formal methods

KW - distributed systems

KW - program verification

KW - concurrency

KW - choreographies

U2 - 10.3990/1.9789036569101

DO - 10.3990/1.9789036569101

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-365-6909-5

T3 - IPA Dissertation Series

PB - University of Twente

CY - Enschede

ER -

Bridging the Implementation Gap: Advancements in Model-Based Concurrent Program Verification

Abstract

Keywords

Access to Document

Fingerprint

Datasets

Artefact of: Verified Parameterized Choreographies

Artefact of: JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java

Artifact of: VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory

Research output

Verified Parameterized Choreographies

VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory

JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java

Cite this