Verified Program: Thread Shared and Back
As you may or may not know, my research work has to do with the verification of object oriented programs, in particular those that are concurrent and use or implement object protocols. The name of my tool is NIMBY, and it's a part of PLURAL which is Kevin's single-threaded verification tool.
I recently was able to mostly verify the implementation of a program that creates an object, shares the object between two threads, and then permanently reacquires thread-local permission to the object. This is sort of a litmus test for many concurrent analyses, and I was quite happy at how naturally it fit into our analysis framework. You can take a look at the verified code here.Other verified programs I tend to post here.
![[info]](http://l-stat.livejournal.com/img/userinfo.gif){kind=small}
nolacoaster) wrote,
