title: Verification of Concurrent Software
keywords: program verification
topics: Logics and semantics
committee: Marieke Huisman

Description

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.

For example:

  • 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.