Connexions

Sections
You are here: Home » Content » Model Checking Concurrent Programs

About: Model Checking Concurrent Programs

Collection type: Course

Course by: Ian Barland, Moshe Vardi, John Greiner. E-mail the authors

View content

Metadata

Name: Model Checking Concurrent Programs
ID: col10294
Language: English (en)
Summary: Introduction to the use of Promela and SPIN as a model-checker for verifying concurrent programs. The underlying transition system is used as a model for the interpretation of Linear Temporal Logic (LTL) formulas.
Collection Subtype: Course
Subject: Science and Technology
Keywords: concurrency, concurrent, deadlock, livelock, LTL, model checking, model-checking, promela, spin, TeachLogic, temporal logic, verification
License: Creative Commons Attribution License CC-BY 2.0
Authors: Ian Barland (ibarland@radford.edu), Moshe Vardi (vardi@cs.rice.edu), John Greiner (greiner@cs.rice.edu)
Copyright Holders: Ian Barland (ibarland@radford.edu), Moshe Vardi (vardi@cs.rice.edu), John Greiner (greiner@cs.rice.edu)
Maintainers: Ian Barland (ibarland@radford.edu), John Greiner (greiner@cs.rice.edu)
Latest version: 1.3 (history)
First publication date: Jul 26, 2005 6:17 pm GMT-5
Last revision to collection: Oct 27, 2005 3:38 pm GMT-5
Collection Structure XML: col10294_1.3_collection.xml
All collection files: col10294_1.3_complete.zip

Version History

Version: 1.3 Oct 27, 2005 3:38 pm GMT-5 by Ian Barland
Changes: 
*Really*, change the name to "model checking ..."
Version: 1.2 Sep 27, 2005 5:49 pm GMT-5 by Ian Barland
Changes: 
Changed course-name.
Version: 1.1 Jul 29, 2005 12:31 pm GMT-5 by Ian Barland
Changes: 
Init.

How to Reuse and Attribute This Content

If you derive a copy of this content using a Connexions account and publish your version, proper attribution of the original work will be automatically done for you.

If you reuse this work elsewhere, in order to comply with the attribution requirements of the license (CC-BY 2.0), you must include

  • the authors' names: Ian Barland, Moshe Vardi, John Greiner
  • the title of the work: Model Checking Concurrent Programs
  • the Connexions URL where the work can be found: http://cnx.org/content/col10294/1.3/

See the citation section below for examples you can copy.

How to Cite and Attribute This Content

The following citation styles comply with the attribution requirements for the license (CC-BY 2.0) of this work:

American Chemical Society (ACS) Style Guide:

Barland, I.; Vardi, M.; Greiner, J. Model Checking Concurrent Programs, Connexions Web site. http://cnx.org/content/col10294/1.3/, Oct 27, 2005.

American Medical Assocation (AMA) Manual of Style:

Barland I, Vardi M, Greiner J. Model Checking Concurrent Programs [Connexions Web site]. October 27, 2005. Available at: http://cnx.org/content/col10294/1.3/.

American Psychological Assocation (APA) Publication Manual:

Barland, I., Vardi, M., & Greiner, J. (2005, October 27). Model Checking Concurrent Programs. Retrieved from the Connexions Web site: http://cnx.org/content/col10294/1.3/

Chicago Manual of Style (Bibliography):

Barland, Ian, Moshe Vardi, and John Greiner. "Model Checking Concurrent Programs." Connexions. October 27, 2005. http://cnx.org/content/col10294/1.3/.

Chicago Manual of Style (Note):

Ian Barland, Moshe Vardi, and John Greiner, "Model Checking Concurrent Programs," Connexions, October 27, 2005, http://cnx.org/content/col10294/1.3/.

Chicago Manual of Style (Reference, in Author-Date style):

Barland, I., Vardi, M., & Greiner, J. 2005. Model Checking Concurrent Programs. Connexions, October 27, 2005. http://cnx.org/content/col10294/1.3/.

Modern Languages Association (MLA) Style Manual:

Barland, Ian, Moshe Vardi, and John Greiner. Model Checking Concurrent Programs. Connexions. 27 Oct. 2005 <http://cnx.org/content/col10294/1.3/>.