Thumbnail
Access Restriction
Subscribed

Author Ben-Ari, Mordechai Moti
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword Erigone ♦ Spin ♦ Model checking ♦ Verification ♦ Concurrent programming
Abstract Model checking is a widely used formal method for the verification of concurrent programs. This article starts with an introduction to the concepts of model checking, followed by a description of Spin, one of the foremost model checkers. Software tools for teaching concurrency and nondeterminism using model checking are described: Erigone, a model checker for teaching; jSpin, a development environment; VN, a visualization of nondeterminism.
Description Affiliation: Weizmann Institute of Science, Rehovot Israel (Ben-Ari, Mordechai Moti)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2013-12-01
Publisher Place New York
Journal Inroads
Volume Number 1
Issue Number 1
Page Count 8
Starting Page 40
Ending Page 47


Source: ACM Digital Library