On Deductive Verification of an Industrial Concurrent Software Component with VerCors
The work
| Title | On Deductive Verification of an Industrial Concurrent Software Component with VerCors |
|---|---|
| Authors | Raúl E. Monti; Robert Rubbens; Marieke Huisman |
| Type | conference paper |
| Year | 2022 |
| Citekey | monti2022deductive |
Where it appeared
| Published in | Leveraging Applications of Formal Methods, Verification and Validation |
|---|---|
| Publisher | Springer |
| Pages | 517--534 |
Identifiers
| DOI | 10.1007/978-3-031-19849-6_29 |
|---|---|
| OpenAlex | W4312481170 |
Access
| Landing page | https://doi.org/10.1007/978-3-031-19849-6_29 |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007/978-3-031-19849-6_29.pdf |
| Link it arrived with | https://link.springer.com/content/pdf/10.1007/978-3-031-19849-6_29.pdf |
Abstract
This paper presents a case study where a concurrent module of a tunnel control system written in Java is verified for memory safety and data race freedom using VerCors, a software verification tool. This case study was carried out in close collaboration with our industrial partner Technolution, which is in charge of developing the tunnel control software. First, we describe the process of preparing the code for verification, and how we make use of the different capabilities of VerCors to successfully verify the module. The concurrent module has gone through a rigorous process of design, code reviewing and unit and integration testing. Despite this careful approach, VerCors found two memory related bugs. We describe these bugs, and show how VerCors could have found them during the development process. Second, we wanted to communicate back our results and verification process to the engineers of Technolution. We discuss how we prepared our presentation, and the explanation we settled on. Third, we present interesting feedback points from this presentation. We use this feedback to determine future work directions with the goal to improve our tool support, and to bridge the gap between formal methods and industry.
Copy held
| Kind | PDF, 284.4 kB |
|---|---|
| Retrieved | 2026-08-08 |
| Held | local, for personal reference |
| Where it came from | https://link.springer.com/content/pdf/10.1007/978-3-031-19849-6_29.pdf?error=cookies_not_supported&code=b5af91c2-e521-4c49-9b51-703305d5cce5 |
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-05 |
| Record | reviewed by a person |
| Approved | 2026-08-16 |
Cite it as
@inproceedings{monti2022deductive,
title = {On Deductive Verification of an Industrial Concurrent Software Component with VerCors},
author = {Raúl E. Monti and Robert Rubbens and Marieke Huisman},
year = {2022},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation},
pages = {517--534},
publisher = {Springer},
doi = {10.1007/978-3-031-19849-6_29},
url = {https://link.springer.com/content/pdf/10.1007/978-3-031-19849-6_29.pdf},
}
This record lives at https://refs.drheap.org/monti2022deductive/ and will keep doing so.