Computer Science · Formal Methods & Verification

Model Checking

A topic within Formal Methods & Verification, itself one of 9 topics in that field and part of Computer Science.

Reading on Model Checking

2 works

Paper1981

Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic

Edmund M. Clarke & E. Allen Emerson

Introduces branching-time temporal logic as a specification language for concurrent programs and an algorithm for checking a finite-state program against it automatically, founding model checking as a field.

Computer Science · Formal Methods & Verification

FreeAdvanced

Paper1997

The Model Checker SPIN

Gerard J. Holzmann

Describes SPIN's design for verifying concurrent software by directly checking process interaction models against linear temporal logic properties, and reports its use finding real protocol bugs.

Computer Science · Formal Methods & Verification

FreeAdvanced

Reading on Model Checking

Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic

The Model Checker SPIN

Other topics in Formal Methods & Verification