Premium
An improvement of partial‐order verification
Author(s) -
Schoot Hans Van Der,
Ural Hasan
Publication year - 1998
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/(sici)1099-1689(199806)8:2<83::aid-stvr157>3.0.co;2-f
Subject(s) - partial order reduction , model checking , computer science , reduction (mathematics) , state space , set (abstract data type) , state (computer science) , linear temporal logic , temporal logic , concurrency , programming language , formal verification , high level verification , algorithm , theoretical computer science , mathematics , software , software development , statistics , geometry , software construction
Abstract Partial‐order reduction methods form a collection of state exploration techniques set to relieve the state‐explosion problem in concurrent program verification. Their use often reduces significantly the memory needed for verifying local and termination properties of concurrent programs and, moreover, for verifying that concurrent programs satisfy their linear‐time temporal logic specifications (i.e. for LTL model‐checking). One particular such method is implemented in the verification system SPIN, which is considered to be one of the most efficient and most widely used LTL model‐checkers. This paper builds on SPIN's partial‐order reduction method to yield an approach that enables further space reductions for verifying concurrent programs. © 1998 John Wiley & Sons, Ltd.