Deadlock and starvation free reentrant readers-writers: A case study combining model checking with theorem proving

Bernard van Gastel; Leonard Lensink; Sjaak Smetsers; Marko van Eekelen

doi:10.1016/j.scico.2010.03.004

Deadlock and starvation free reentrant readers-writers: A case study combining model checking with theorem proving

Bernard van Gastel, Leonard Lensink, Sjaak Smetsers, Marko van Eekelen^*

^*Corresponding author for this work

Research output: Contribution to journal › Article › Academic › peer-review

Original language	English
Pages (from-to)	82-99
Number of pages	18
Journal	Science of Computer Programming
Volume	76
Issue number	2
DOIs	https://doi.org/10.1016/j.scico.2010.03.004
Publication status	Published - 1 Feb 2011

Keywords

Model checking
Theorem proving
Readers-writers algorithm
SPIN
PVS
VERIFICATION
JAVA

Access to Document

10.1016/j.scico.2010.03.004

Cite this

@article{08215e4fd5ad41f3b13c947b8ce89211,

title = "Deadlock and starvation free reentrant readers-writers: A case study combining model checking with theorem proving",

keywords = "Model checking, Theorem proving, Readers-writers algorithm, SPIN, PVS, VERIFICATION, JAVA",

author = "{van Gastel}, Bernard and Leonard Lensink and Sjaak Smetsers and {van Eekelen}, Marko",

year = "2011",

month = feb,

day = "1",

doi = "10.1016/j.scico.2010.03.004",

language = "English",

volume = "76",

pages = "82--99",

journal = " Science of Computer Programming",

issn = "0167-6423",

publisher = "ELSEVIER SCIENCE BV",

number = "2",

}

TY - JOUR

T1 - Deadlock and starvation free reentrant readers-writers

T2 - A case study combining model checking with theorem proving

AU - van Gastel, Bernard

AU - Lensink, Leonard

AU - Smetsers, Sjaak

AU - van Eekelen, Marko

PY - 2011/2/1

Y1 - 2011/2/1

KW - Model checking

KW - Theorem proving

KW - Readers-writers algorithm

KW - SPIN

KW - PVS

KW - VERIFICATION

KW - JAVA

U2 - 10.1016/j.scico.2010.03.004

DO - 10.1016/j.scico.2010.03.004

M3 - Article

SN - 0167-6423

VL - 76

SP - 82

EP - 99

JO - Science of Computer Programming

JF - Science of Computer Programming

IS - 2

ER -

Deadlock and starvation free reentrant readers-writers: A case study combining model checking with theorem proving

Keywords

Access to Document

Fingerprint

Cite this