Leto - Verifying Application-Specific Fault Tolerance through Parameterized Execution Models

on YouTube ↗23m

" summary

Leto is an SMT-based verifier that lets developers encode hardware fault semantics and prove relational properties between a fault-free and a relaxed execution. It implements SMT-based verifier checks, automatic loop invariant inference and relational assertions over single-event upset models and multiplicative/additive variants. The paper verifies four self-stabilizing algorithms plus vector product under five execution models, infers most loop invariants (reducing manual annotations), generates Z3 constraints, and reports modest memory and seconds-scale verification times, demonstrating the approach works on realistic examples.

AI-written summary · about

" chapters (13)

1. 0:00Start
2. 1:41Single Event Upset
3. 3:15Application Specific Hardware Fault Tolerance
4. 5:44System Overview Leto Execution Model
5. 6:47Vector Product: DMR
6. 8:38Relative Error Model
7. 9:27Bounded Error Vector Product
8. 11:24Summary
9. 11:58Hardware Model Semantics
10. 12:28Relational Program Logic
11. 14:24DMR Example (Lockstep)
12. 15:08Benchmarks: Programs
13. 15:37Benchmarks: Execution Models