Input-based Three-Valued Abstraction Refinement
summary
A new three-valued abstraction refinement framework implements input-based splitting and a simulator-like abstract state construction in the open-source tool machine-check, targets AVR machine code, and supports full mu-calculus model checking. It verifies properties that CEGAR and naïve model checking cannot, finds a real bug in an AVR voltage-controlled-oscillator calibration program (the LSB of a trim value is never cleared), and produces reasonable runtimes on several embedded benchmarks.
AI-written summary · about
chapters (15)
- 0:00Temporal logic model checking
- 1:51Path universal properties limits
- 3:58Three-valued abstraction refinement
- 5:22Three-valued model checking challenges
- 7:07Input-based three-valued refinement
- 12:26Abstract simulation input splitting
- 14:12Decay to control state explosion
- 15:39Tool implementation results
- 18:09Future research directions
- 19:14Conclusion adoption challenges
- 19:36Q&A: Certificates
- 21:21Q&A: State abstraction
- 23:27Q&A: Real-world evaluation
- 26:17Q&A: Decay role
- 28:25Q&A: Bug details
related talks
45mDesign and implementation of a verified interpreter for additive manufacturing programs
54mCost of Abstractions in Embedded Systems
21mDeductive Verification of Parameterized Embedded Systems modeled in SystemC
32mSecSi Product Development
28mReactive Programming on the Bare Metal:A Formal Model for a Low-Level Reactive Virtual Machin
21mThe New Verification Ecosystem that Supports RISC-V Verification fo...
24mContinuous VHDL inspection with opensource software
13mEarly RISC-V Software Verification with SIM-V