AI Snips
Chapters
Transcript
Episode notes
Verification's Practical Limits
- Verification aims to prove source programs meet specifications but is undecidable in general.
- Greta moved from pure verification to combining formal methods with practical tooling to help real users.
Merge Tests With Formal Abstraction
- Combining concrete execution with abstraction generalizes observed states and boosts verification coverage.
- Use counterexample-guided runs to discover untested states and expand testing or proofs.
Arm Work Sparked Super-Optimization
- At Arm Greta saw tight hardware/compiler interactions and felt constrained by separate passes.
- That motivated interest in super-optimization to search globally for optimal instruction sequences.