@phdthesis{Rubbens2025,
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.",
author = "Robert B. Rubbens",
year = "2025",
month = "10",
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"
}

{"_id":"uCrnsFwmuBjkrWTsm","bibbaseid":"rubbens-bridgingtheimplementationgapadvancementsinmodelbasedconcurrentprogramverification-2025","author_short":["Rubbens, R. B."],"bibdata":{"bibtype":"phdthesis","type":"PhD Thesis - Research UT, graduation UT","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.","author":[{"firstnames":["Robert","B."],"propositions":[],"lastnames":["Rubbens"],"suffixes":[]}],"year":"2025","month":"10","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","school":"University of Twente","bibtex":"@phdthesis{Rubbens2025,\ntitle = \"Bridging the Implementation Gap: Advancements in Model-Based Concurrent Program Verification\",\nabstract = \"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.\",\nauthor = \"Robert B. Rubbens\",\nyear = \"2025\",\nmonth = \"10\",\nday = \"15\",\ndoi = \"10.3990/1.9789036569101\",\nlanguage = \"English\",\nisbn = \"978-90-365-6909-5\",\nseries = \"IPA Dissertation Series\",\npublisher = \"University of Twente\",\nnumber = \"14\",\naddress = \"Netherlands\",\ntype = \"PhD Thesis - Research UT, graduation UT\",\nschool = \"University of Twente\"\n}\n\n","author_short":["Rubbens, R. B."],"key":"Rubbens2025","id":"Rubbens2025","bibbaseid":"rubbens-bridgingtheimplementationgapadvancementsinmodelbasedconcurrentprogramverification-2025","role":"author","urls":{},"metadata":{"authorlinks":{}},"html":""},"bibtype":"phdthesis","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","dataSources":["cCvCnPTRQYq3qPe9y"],"keywords":[],"search_terms":["bridging","implementation","gap","advancements","model","based","concurrent","program","verification","rubbens"],"title":"Bridging the Implementation Gap: Advancements in Model-Based Concurrent Program Verification","year":2025}