02MC

Foreword

This sequel is intended as a hands-on introduction to formal verification by model-checking (mostly explicit-state), even though a more sophisticated reader might see opportunities for symbolic or mixed explicit-symbolic verification.

After engaging with the content here a reader interested in using formal verification shall have the necessary background to understand deeply some of the existing model-checking tools: TLA+, SPIN, UPPAAL.

After engaging with the content here a reader working on language design might be willing to try designing (and implementing) the semantics of the language through the piecewise relation abstraction, which offers a bridge between behavioral language semantics (seen as specifications) and behavioral verification tools.

Games