Temporal Modal Logic: The Time is Now
summary
Claims that temporal modal logics enable practical, automated verification: LTL and CTL become executable specs, model checking produces concrete counterexamples (first hardware bug found in a FIFO in a few nights), and chip design now uses a temporal assertion language (SystemVerilog) to vet designs with billions of transistors. Concrete failures motivate it: one bad Intel floating point division in ~9 billion costs ~$475M. A new tool called modality aims to make these logics learnable and usable for verifiable systems.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 2:52Command versus govern in computing
- 7:05Aristotle's logic contributions
- 12:43Leibniz to Frege and formal logic
- 16:33Gödel, Lewis, and modal semantics
- 18:00Temporal logic and Arthur Prior
- 19:48Linear versus branching time
- 21:54Hardware verification with temporal logic
- 22:59Why temporal logic is hard
- 23:41New temporal logic system
- 27:57Box and diamond operators
- 30:03Recursion in temporal logic
- 31:46Temporal logic in prisoner's dilemma
- 32:49Verifiable contracts and future apps
related talks
15mConveros: Practical Model Checking for Verifying Rust OS Kernel Concurrency
17mSoftware Transaction Memory, For Reals
20mModular Specification and Verification of Closures in Rust
54mCompile-Time Validation in C++ Programming
01h 02mHardware/Software Co-design: The Coming Golden Age
43mTick Tock: Maintaining Time
21mMisusing Const for Fn and Profit
31mDefense Against The Wrong Logic: Proactive Rust Coding