Preview: Verification (Correctness)
summary
Five papers show concrete claims and artifacts: data-driven environment synthesis uses protocol traces to prune and order invariant candidates so fewer solver queries are needed; verified concurrent journaling implements and machine-verifies a crash-safe journaling layer and a simplified verified NFSv3 core; refinement types for web security lets developers express data-dependent policies in a central file and checks them statically; automated JS parallelization splits server/client work to schedule web workers and reports large speedups; hybrid static-dynamic redundancy elimination cuts runtime checker overhead (address checkers cost up to 33%).
AI-written summary · about
chapters (20)
- 0:00Intro
- 0:18What is correctness?
- 0:43Bugs are widespread
- 1:22Bugs are costly.
- 1:37Tackling Bugs in Different Stages
- 2:49Static Checking
- 5:11Formal Verification: model checking
- 6:20Formal Verification: theorem proving
- 7:26Testing Overview
- 7:51Symbolic Execution
- 8:28Fuzz Testing
- 9:18Logging
- 9:51Dynamic Checking • Analyze the execution following bug patterns
- 10:24Failure Prevention
- 10:40Patching
- 11:16Verification Papers
- 13:43GoJournal
- 14:36STORM
- 15:43Horcrux
- 16:50SANRAZOR
related talks
38mThe Verification of a Distributed System
20mNegative/Positive Verification for WorldGuard, CHERI and Other RISC-V Security Models-
21mCombined Dynamic and Formal Verification Approach to Processor Verification
23mBeyond Tests What to Verify in AI Generated Code
46mIntroduction to Formal Verification with Symbiotic EDA Open Source Tools
15mGradual Verification of Recursive Heap Data Structures
47mTutorial: Choosing Appropriate Verification Techniques for Desired RISC...
25mApplying Program Verification to Linux Kernel Code: Challenges, Practices, and...