@techreport{ball2000parameterized,
author = {Ball, Thomas and Chaki, Sagar and Rajamani, Sriram},
title = {Parameterized Verification of Multithreaded Software Libraries},
institution = {Microsoft},
year = {2000},
month = {December},
abstract = {The growing popularity of multi-threading has led to a great number of software libraries that support access by multiple threads. We present Local/Global Finite State Machines (LGFSMs) as a model for a certain class of multithreaded libraries. We have developed a tool called Beacon that does parameterized model checking of LGFSMs . We demonstrate the expressiveness of LGFSMs as models, and the effectiveness of Beacon as a model checking tool by (1) modeling a multithreaded memory manager Rockall developed at Microsoft Research as an LGFSM , and (2) using Beacon to check a critical safety property of Rockall.},
url = {http://approjects.co.za/?big=en-us/research/publication/parameterized-verification-of-multithreaded-software-libraries/},
number = {MSR-TR-2000-116},
}