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 at this link: paypalme. You can also scan this QR code for a payment via Venmo (the name says Edsger Studio, which is my payment site).
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)
| Topic | m:s | quiz | ||
|---|---|---|---|---|
| Intro 1 of 2 | 32:48 | transcript | ||
| Intro 2 of 2 | 35:53 | transcript | ||
| Uno | 23:23 | files | ||
| Uno demo | 13:26 | transcript | Excercises | |
| Coverity | 09:16 | transcript | ||
| Coverity demo | 14:07 | transcript | ||
| Codesonar/Semmle | 12:47 | 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 | 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.'
| Topic | m:s | quiz | ||
|---|---|---|---|---|
| Overview (52 min) | ||||
| Intro 1 of 3 | 14:53 | 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 | 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:55 | files | 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 | files | Q2b1 | |
| Verification-II 2 of 3 (transition fairness, ltl) | 24:54 | transcript | AL2b | |
| Verification-II 3 of 3 (the Buzz tool) | 24:22 | transcript | AL2c | |
| Theory (1 h 12 min) | ||||
| Automata 1 of 5 (FSA, NFSA) | 07:26 | 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 | files | Q3b1 | |
| LTL 2 of 2 (non-progress, CTL*, CTL) | 22:32 | transcript | Q3b2 | |
| Algorithms (1 h 40 min) | ||||
| Algorithms (DFS, BFS) | 15:27 | files | Q4a1 | |
| Algorithms (Depth-bounded Search) | 09:46 | transcript | Q4a2 | |
| files | Q4b | |||
| - | ||||
| Storage 1 of 4 (complexity, collapse) | 15:12 | 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 | 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