When developing a concurrent program, a deadlock is never the intended result. However, avoiding them is often attributed to the experience of the developer, as a compiler is generally not able to detect them. Recently, a technique has been proposed to verify deadlock-freeness of a program with monitors. The aim of this research is to investigate how this technique can be encoded in the VerCors verification tool to verify deadlock-freeness of Java-like programs. This paper specifies the required annotation syntax and describes the implementation of the technique in VerCors.
The Research Project is a research project that serves as an exercise for the master’s thesis. As such it serves to give master students who did their bachelor study elsewhere the experience that bachelor students from the UT obtained during their bachelor project.
View the full research paper for this project.
When developing a concurrent program, a deadlock is never the intended result. However, avoiding them is often attributed to the experience of the developer, as a compiler is generally not able to detect them. Recently, a technique has been proposed to verify deadlock-freeness of a program with monitors. The aim of this research is to investigate how this technique can be encoded in the VerCors verification tool to verify deadlock-freeness of Java-like programs. This paper specifies the required annotation syntax and describes the implementation of the technique in VerCors.
The Research Project is a research project that serves as an exercise for the master’s thesis. As such it serves to give master students who did their bachelor study elsewhere the experience that bachelor students from the UT obtained during their bachelor project.
View the full research paper for this project.