Case Studies

This page lists all the case studies that have been done with VerCors.

Published case studies

• Automated Verification of the Parallel Bellman-Ford Algorithm. M. Safari, W. Oortwijn and M. Huisman (SAS 2021).
  • Paper: https://doi.org/10.1007/978-3-030-88806-0_17
  • Code: https://github.com/Safari1991/SSSP-Verification
  • Builds on the student project by J. Smits
• Permission-Based Verification of Red-Black Trees and Their Merging. L. Armborst and M. Huisman (FormaliSE 2021).
  • Paper: https://research.utwente.nl/en/publications/permission-based-verification-of-red-black-trees-and-their-mergin
  • Code: https://data.4tu.nl/articles/software/_/13611578
  • This is a continuation of the master project by H.M. Nguyen
• Formal Verification of Parallel Stream Compaction and Summed-Area Table Algorithms. M. Safari and M. Huisman (ICTAC 2020).
  • Paper: https://doi.org/10.1007/978-3-030-64276-1_10
  • Code: https://github.com/Safari1991/Prefixsum-Applications
• A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms. M. Safari and M. Huisman (IFM 2020).
  • Paper: https://doi.org/10.1007/978-3-030-63461-2_14
  • Code: https://github.com/Safari1991/Permutation
• On the Industrial Application of Critical Software Verification with VerCors. M. Huisman and R.E. Monti (ISoLA 2020).
  • Paper: https://doi.org/10.1007/978-3-030-61467-6_18
  • Code: Not publicly available
  • This was in collaboration with the companies Technolution and Thales.
  • This case study uses a combination of mCRL2 (model checker) and VerCors to prove correctness of the software.
• Formal Verification of Parallel Prefix Sum. M Safari, W. Oortwijn, S. Joosten and M. Huisman (NFM 2020).
  • Paper: https://doi.org/10.1007/978-3-030-55754-6_10
  • Code: https://github.com/Safari1991/Prefixsum
  • Builds on the student project by T. Wiefferink
• Automated Verification of Parallel Nested DFS. W. Oortwijn, M. Huisman, S.J.C. Joosten and J. van de Pol (TACAS 2020).
  • Paper: https://doi.org/10.1007/978-3-030-45190-5_14
  • Code: https://doi.org/10.4121/uuid:36c00955-5574-44d9-9b26-340f7a1ea03b
• Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System. W. Oortwijn and M. Huisman (IFM 2019).
  • Paper: https://doi.org/10.1007/978-3-030-34968-4_23
  • Code: Not publicly available
  • This was in collaboration with the company Technolution.
  • This case study uses a combination of mCRL2 (model checker) and VerCors to prove correctness of the software.

Student projects

Be aware that not all student projects verify complete functional correctness!

Master projects

• Verification of a model checking algorithm in VerCors. H. Hollander (2021).
  • Master thesis: http://purl.utwente.nl/essays/88268
  • Code: https://github.com/HanHollander/SetBasedSCC
• Formal verification of a red-black tree data structure. H.M. Nguyen (2019).
  • Master thesis: http://purl.utwente.nl/essays/77569
  • Code: https://fmt.ewi.utwente.nl/media/rbt.zip
  • This has been continued in Permission-Based Verification of Red-Black Trees and Their Merging (more info in the published case studies list above)

Bachelor projects

• Let's sort this out: GPGPU Verification of Radix Sort. D.H.M.A. van Oorschot (2020).
  • Bachelor thesis: http://purl.utwente.nl/essays/80589
  • Code: Parallel count algorithm, Parallel reorder algorithm, and Parallel radix sort algorithm.
• GPGPU Verification: Correctness of Odd-Even Transposition Sort Algorithm. Y. Kumashev (2020).
  • Bachelor thesis: http://purl.utwente.nl/essays/80585
  • Code: https://doi.org/10.6084/m9.figshare.11725848.v1
• Formal Automated Verification of a Work-Stealing Deque. C.M. van Kampen (2020).
  • Bachelor thesis: http://purl.utwente.nl/essays/80687
  • Code: https://github.com/coenvk/lace-vercors
• Verifying GPGPU Implementation of Breadth-First Search Algorithm. J. Smits (2019).
  • Bachelor thesis: https://fmt.ewi.utwente.nl/media/Bachelor_Thesis_Jan_Smits_BFS_Verification_1.2.pdf
  • Code: In bachelor thesis
• Optimization, Specification and Verification of the Prefix Sum Program in an OpenCL Environment. T. Wiefferink (2015).
  • Bachelor thesis: https://fmt.ewi.utwente.nl/media/147.pdf
  • Code: https://fmt.ewi.utwente.nl/media/147_attachment_1.zip, also available at: https://github.com/NLthijs48/PrefixSumVerification