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

DOI10.1016/j.scico.2010.03.004zbMath1213.68193OpenAlexW2171982732MaRDI QIDQ617922

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

Publication date: 14 January 2011

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2010.03.004

zbMATH Keywords

theorem provingspinmodel checkingPVSconcurrent softwarereaders-writers algorithm

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

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

Uses Software

• Coq
• Zing
• SPIN
• PVS
• Uppaal
• jSpin
• Java PathFinder
• Bandera
• CESAR
• JPF-SE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Model checking JAVA programs using JAVA PathFinder
• Uppaal in a nutshell
• Code-carrying theories
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification

This page was built for publication: Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving