Syllabus for In-Depth Course on Logic Model Checking


The following is an overview of the main parts of the in-depth course on logic model checking with Spin. As a bonus, it also includes a segment on Static Source Code Analys, that you can skip (it's not needed for the Logic Model Checking part).

Up to date sources for the tools used is available on github (see: nimble-code).

Access

Unlimited access to the course material is available for a single payment of $150 through paypal:

When I see your payment, I will send you the URL and the credentials you'll need to access the course material (typically within a few hours).


Static Source Code Analysis


Lectures (3 h 32 min)

    Topicm:spdf quiz
    Intro 1 of 2 32:48 pdf transcript
    Intro 2 of 2 35:53 pdf transcript
    Uno 23:23 pdf files
    Uno demo 13:26 transcript Excercises
    Coverity 09:16 pdf transcript
    Coverity demo 14:07 transcript
    Codesonar/Semmle 12:47 pdf transcript
    Cobra part 1 of 3 18:30 transcript Q1
    Cobra part 2 of 3 16:57 transcript Q2
    Cobra part 3 of 3 17:19 pdf files Q3
    Cobra demo 17:40 transcript Excercises

Tool Downloads and Links

  • Uno
    • website
    • paper, manual
    • sources
  • Cobra
    • website
    • paper, manual
    • Executables
      • Linux 64-bit
      • Cygwin/Windows 32-bit
      • Mac/OS-X 64-bit


Logic Model Checking & Software Model Extraction


Lectures (10 h)

    • For all assignments use Spin Version 6.4.8 or later.
    • The recorded lectures in mp4 format can be selected in the left column below.
    • A pdf of the slides for each set of lectures can be found under 'pdf.'
    • Transcripts and examples can be found under 'files.'
    Topicm:s quiz
    Overview (52 min)
    Intro 1 of 3 14:53 pdf files
    Intro 2 of 3 15:40 transcript
    Intro 3 of 3 22:05 transcript AL1
    Specification (2 h 4 min)
    Promela-I 1 of 8 (building blocks) 12:20 pdf files Q1a1
    Promela-I 2 of 8 (processes) 14:34 transcript Q1a2
    Promela-I 3 of 8 (basic statements) 15:54 transcript Q1a3
    Promela-I 4 of 8 (compound statements) 08:15 transcript Q1a4
    Promela-I 5 of 8 (loops) 06:59 transcript Q1a5
    Promela-I 6 of 8 (atomic and d_step sequences) 09:56 transcript Q1a6
    Promela-I 7 of 8 (message passing) 16:07 transcript Q1a7
    Promela-I 8 of 8 (data objects) 11:50 transcript AL1a
    -

    files Q1b1
    Promela-II 2 of 3 (preprocessing / priority) 14:25 transcript Q1b2
    Promela-II 3 of 3 (unless sequences) 04:49 transcript AL1b
    Verification (2 h 8 min)
    files
    Verification-I 1 of 3 (safety, liveness, non-progress) 11:55files Q2a1
    Verification-I 2 of 3 (scheduling fairness) 05:29 transcript Q2a2
    Verification-I 3 of 3 (acceptance) 12:41 transcript AL2a
    -

    Verification-II 1 of 3 (never claims) 16:50 pdf files Q2b1
    Verification-II 2 of 3 (transition fairness, ltl) 24:54 transcript AL2b
    Verification-II 3 of 3 (the Buzz tool) 24:22 pdf transcript AL2c
    Theory (1 h 12 min)
    Automata 1 of 5 (FSA, NFSA) 07:26 pdf files Q3a1
    Automata 2 of 5 (Runs, Acceptance) 13:03 transcript Q3a2
    Automata 3 of 5 (Omega Acceptance) 03:20 transcript Q3a3
    Automata 4 of 5 (Stutter Extension) 04:00 transcript Q3a4
    Automata 5 of 5 (Products) 13:03 transcript Q3a5
    -

    LTL 1 of 2 (Kripke structs, link with w-automata) 10:48 pdf files Q3b1
    LTL 2 of 2 (non-progress, CTL*, CTL) 22:32 transcript Q3b2
    Algorithms (1 h 40 min)
    Algorithms (DFS, BFS) 15:27 pdf files Q4a1
    Algorithms (Depth-bounded Search) 09:46 transcript Q4a2
    files Q4b
    -

    Storage 1 of 4 (complexity, collapse) 15:12 pdf files Q4c1
    Storage 2 of 4 (minimized automata) 02:39 transcript Q4c2
    Storage 3 of 4 (bitstate, Bloom filters) 15:50 transcript Q4c3
    Storage 4 of 4 (iterative, hashcompact) 05:53 transcript Q4c4
    -

    files Q4d
    Parallelism (56 min)
    files Q4e
    files Q4f
    files Q4g
    Model Extraction (1 h 2 min)
    Model Extraction Basics 1 of 3 06:24 pdf files Q5a1
    Model Extraction Basics 2 of 3 17:58 transcript Q5a2
    Model Extraction Basics 3 of 3 08:59 transcript AL5a
    -

    files AL5b

Tool Downloads and Links

  • Spin
    • website
    • sources
    • ispin source
    • tau source
  • Buzz
    • sources
  • Modex
    • website
    • sources