PV5 SPINanalyses models of multi-threaded applications with different message passing paradigms or shared memory communication

Application domain/field

Type of tool

Model checker + simulator

Expected input

Format:

PROMELA

Expected output

It reports on deadlocks, race conditions, different types of incompleteness, unwarranted assumptions about the relative speed of processes, and property violations.

Internals

Spin is a open-source software verification tool for formal verification of multi-threaded software applications. It can be used in four main modes: (source: https://spinroot.com/spin/what.html)

Comments

License: BSD 3-clause open source license
Concurrency LTL Model checking Simulation

Links

Related papers

Last publication date

2012

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.