2023-03-03
VeyMont: Parallelising verified programs instead of verifying parallel programs
Publication
Publication
Presented at the
25th International Symposium on Formal Methods, FM 2023 (March 2023), Lübeck, Germany
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).
| Additional Metadata | |
|---|---|
| doi.org/10.1007/978-3-031-27481-7_19 | |
| Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence | |
| 25th International Symposium on Formal Methods, FM 2023 | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
van den Bos, P., & Jongmans, S. (2023). VeyMont: Parallelising verified programs instead of verifying parallel programs. In International Symposium on Formal Methods, FM 2023 (pp. 321–339). doi:10.1007/978-3-031-27481-7_19 |
|
