PPA 9/10: Model Checking [program analysis crash course]
A lecture for BSc students in Innopolis University.
Blog: https://www.yegor256.com
Books: https://www.yegor256.com/books.html
GitHub: https://github.com/yegor256 (don’t hesitate to follow in order to stay informed)
Telegram channel with recent news and updates: https://t.me/yegor256news (subscribe to not miss a thing)
Twitter with daily and weekly updates: / yegor256 (follow me!)
iTunes: https://podcasts.apple.com/us/podcast...
SoundCloud: / yegor256
Yandex Music podcast by yegor256: https://music.yandex.ru/album/31142286
0:00 Introduction
3:43 Motivating Example. Div by Zero
11:13 ProMela (Process Meta Language)
20:48 SPIN (Simple ProMela Interpreter)
23:05 Monitoring Process
25:55 Fail on Assertion
39:53 Theory. The Idea
48:05 The Model
48:40 Linear Temporal Logic
53:19 Model-less Model Checking. Race Condition
58:17 States and Their Explosion
1:02:18 Java PathFinder
1:08:24 ChatGPT
1:12:20 Conclusion