Bernard van Gastel, Leonard Lensink, Sjaak Smetsers, Marko C. J. D. van Eekelen. Deadlock and starvation free reentrant readers-writers: A case study combining model checking with theorem proving. Science of Computer Programming, 76(2):82-99, 2011. [doi]
Abstract is missing.