|title:||Verification of Concurrent Software|
|topics:||Logics and semantics|
Within the FMT group, since several years we are working on the development of the VerCors verifier, which aims in particular at the verification of concurrent software. Many different projects related to VerCors are possible.
- extending the theory of program verification
- improving practical support for VerCors
- developing verification case studies (e.g. verifying an ArrayList, LinkedList, Hashtable)
- investigating how to enlarge the class of properties that can be verified
If you are interested in such a project, feel free to contact me and to discuss the possibilities.
For more information about VerCors, see the VerCors webpage.