This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Marieke Huisman
A grouping.
Verification of concurrent and parallel programs, and the question of whether it pays. The tool is VerCors, with permission-based separation logic for multithreaded Java underneath it, magic wands, and JML on the specification side. Three further records report what happens when industry is asked to use such a method -- a travel guide from academia to industrial practice, critical software verification, and a deductive verification of an industrial concurrent component -- which is an unusual thing to hold beside the verifier itself. dblp: https://dblp.org/pid/76/6612
9 references
On Deductive Verification of an Industrial Concurrent Software Component with VerCors
Raúl E. Monti and others (2022) · Leveraging Applications of Formal Methods, Verification and Validation · Springer
Permission-based verification of red-black trees and their merging
Lukas Armborst and others (2021) · 2021 IEEE/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE) · IEEE
Formal Methods: From Academia to Industrial Practice. A Travel Guide
Marieke Huisman and others (2020) · arXiv
On the Industrial Application of Critical Software Verification with VerCors
Marieke Huisman and others (2020) · Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020) · Springer International Publishing
The VerCors Tool Set: Verification of Parallel and Concurrent Software
Stefan Blom and others (2017) · Integrated Formal Methods · Springer
Permission-based separation logic for multithreaded Java programs
Afshin Amighi and others (2015) · Logical Methods in Computer Science
Witnessing the elimination of magic wands
Stefan Blom and others (2015) · International Journal on Software Tools for Technology Transfer · Springer
The VerCors tool for verification of concurrent programs
Stefan Blom and others (2014) · International Symposium on Formal Methods · Springer
Formal Specification with JML
Marieke Huisman and others (2014) · Karlsruhe Institute of Technology