@misc{essay82062,
title       = {Encoding deadlock-free monitors in the VerCors verification tool},
month       = {July},
year        = {2020},
author      = {M.J. {Roelink}},
abstract    = {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.},
url         = {http://essay.utwente.nl/82062/}
}

{"_id":"GjhHbwmXtasnPYyT2","bibbaseid":"roelink-encodingdeadlockfreemonitorsinthevercorsverificationtool-2020","authorIDs":[],"author_short":["Roelink, M."],"bibdata":{"bibtype":"misc","type":"misc","title":"Encoding deadlock-free monitors in the VerCors verification tool","month":"July","year":"2020","author":[{"firstnames":["M.J."],"propositions":[],"lastnames":["Roelink"],"suffixes":[]}],"abstract":"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.","url":"http://essay.utwente.nl/82062/","bibtex":"@misc{essay82062,\ntitle = {Encoding deadlock-free monitors in the VerCors verification tool},\nmonth = {July},\nyear = {2020},\nauthor = {M.J. {Roelink}},\nabstract = {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.},\nurl = {http://essay.utwente.nl/82062/}\n}\n\n","author_short":["Roelink, M."],"key":"essay82062","id":"essay82062","bibbaseid":"roelink-encodingdeadlockfreemonitorsinthevercorsverificationtool-2020","role":"author","urls":{"Paper":"http://essay.utwente.nl/82062/"},"metadata":{"authorlinks":{}},"downloads":1},"bibtype":"misc","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","creationDate":"2020-11-06T08:40:48.490Z","downloads":1,"keywords":[],"search_terms":["encoding","deadlock","free","monitors","vercors","verification","tool","roelink"],"title":"Encoding deadlock-free monitors in the VerCors verification tool","year":2020,"dataSources":["2tJugFYAignELAmZo","zT4KxAXTKvhK2Hrr4","cCvCnPTRQYq3qPe9y"]}