PVS vs SPIN

PVS is a mechanized environment for formal specification and verification, intended for work such as mathematical formalization and hardware or algorithm verification. Its language is based on typed higher-order logic and supports predicate subtypes, dependent types, and parameterized theories. The system combines predefined theories, a type checker, interactive theorem prover, symbolic model checker, utilities, libraries, documentation, and examples. Proof support includes induction, rewriting, simplification with decision procedures, abstraction, and symbolic model checking; command-line tools can re-prove theories and libraries in batch mode. PVS also integrates the Yices SMT solver, supports random testing during proofs, and includes PVSio for evaluation and animation. GNU or X Emacs provides the integrated interface, with Tcl/Tk displays for proof trees and theory hierarchies. It runs on Linux, macOS, and Windows and is self-hosted. Noncommercial use is listed at free. Sources are under GPL, but the Allegro runtime has a separate click-through license, and commercial users need a current PVS license or must contact SRI about licensing.

SPIN is a free, self-hosted model-checking tool for analyzing the logical consistency of asynchronous systems, including distributed software and communication protocols. Systems are specified in Promela, which represents asynchronous processes, nondeterministic choices, loops, and local or global variables. Models can state correctness requirements, including linear temporal logic. SPIN supports interactive, guided, and random simulations of execution. For verification, it generates a C program for exhaustive or approximate checking of those requirements. Its product description lists detection of deadlocks, race conditions, incomplete specifications, and unjustified assumptions about process speeds. Partial order reduction optimizes verification runs, while the site provides guidance for multicore depth-first and breadth-first algorithms and swarm methods for large state spaces. SPIN runs on Linux, macOS, and Windows, as well as other listed systems. From version 6.4.5, its code, sources, and executables use the BSD 3-Clause license. Verification requires a working C compiler and preprocessor. The optional iSpin graphical interface is written in Tcl/Tk and requires Tcl/Tk.