@article{vanGastel2010, title = "Deadlock and starvation free reentrant readers-writers--a case study combining model checking with theorem proving", journal = "Science of Computer Programming", volume = "76", number = "2", pages = "82-99", year = "2011", note = "Selected papers from the workshops on Formal Methods for Industrial Critical Systems - FMICS 2007 + FMICS 2008", issn = "0167-6423", doi = "DOI: 10.1016/j.scico.2010.03.004", url = "http://www.sciencedirect.com/science/article/B6V17-509XPN2-2/2/54abfac6d01c4b7389273b2c697a2926", author = "Bernard van Gastel and Leonard Lensink and Sjaak Smetsers and Marko van Eekelen", keywords = "Model checking", keywords = "Theorem proving", keywords = "Readers-writers algorithm", keywords = "Spin", keywords = "PVS" }