Multi-core model checking with Spin

G.J. Holzmann; D. Bosnacki

doi:10.1109/IPDPS.2007.370410

Multi-core model checking with Spin

G.J. Holzmann, D. Bosnacki

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

20 Citations (Scopus)

Abstract

We present the first experimental results on the implementation of a multi-core model checking algorithm for the SPIN model checker. These algorithms specifically target shared-memory systems, and are initially restricted to dual-core systems. The extensions we have made require only small changes in the SPIN source code, and preserve virtually all existing verification modes and optimization techniques supported by SPIN, including the verification of both safety and liveness properties and the verification of SPIN models with embedded C code fragments.

Original language	English
Title of host publication	Proceedings of the 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), 26-30 March 2007, Long Beach CA, USA
Place of Publication	United States, Long Beach, California
Publisher	Institute of Electrical and Electronics Engineers
Pages	1-8
DOIs	https://doi.org/10.1109/IPDPS.2007.370410
Publication status	Published - 2007

Access to Document

10.1109/IPDPS.2007.370410

Cite this

@inproceedings{86bca574c9794da2b45bcd168601495a,

title = "Multi-core model checking with Spin",

abstract = "We present the first experimental results on the implementation of a multi-core model checking algorithm for the SPIN model checker. These algorithms specifically target shared-memory systems, and are initially restricted to dual-core systems. The extensions we have made require only small changes in the SPIN source code, and preserve virtually all existing verification modes and optimization techniques supported by SPIN, including the verification of both safety and liveness properties and the verification of SPIN models with embedded C code fragments.",

author = "G.J. Holzmann and D. Bosnacki",

year = "2007",

doi = "10.1109/IPDPS.2007.370410",

language = "English",

pages = "1--8",

booktitle = "Proceedings of the 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), 26-30 March 2007, Long Beach CA, USA",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

}

Multi-core model checking with Spin. / Holzmann, G.J.; Bosnacki, D.
Proceedings of the 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), 26-30 March 2007, Long Beach CA, USA. United States, Long Beach, California: Institute of Electrical and Electronics Engineers, 2007. p. 1-8.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Multi-core model checking with Spin

AU - Holzmann, G.J.

AU - Bosnacki, D.

PY - 2007

Y1 - 2007

N2 - We present the first experimental results on the implementation of a multi-core model checking algorithm for the SPIN model checker. These algorithms specifically target shared-memory systems, and are initially restricted to dual-core systems. The extensions we have made require only small changes in the SPIN source code, and preserve virtually all existing verification modes and optimization techniques supported by SPIN, including the verification of both safety and liveness properties and the verification of SPIN models with embedded C code fragments.

AB - We present the first experimental results on the implementation of a multi-core model checking algorithm for the SPIN model checker. These algorithms specifically target shared-memory systems, and are initially restricted to dual-core systems. The extensions we have made require only small changes in the SPIN source code, and preserve virtually all existing verification modes and optimization techniques supported by SPIN, including the verification of both safety and liveness properties and the verification of SPIN models with embedded C code fragments.

U2 - 10.1109/IPDPS.2007.370410

DO - 10.1109/IPDPS.2007.370410

M3 - Conference contribution

SP - 1

EP - 8

BT - Proceedings of the 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), 26-30 March 2007, Long Beach CA, USA

PB - Institute of Electrical and Electronics Engineers

CY - United States, Long Beach, California

ER -

Multi-core model checking with Spin

Abstract

Access to Document

Fingerprint

Cite this