Multi-Aspect Verification in Practice
Checking multiple verification properties in a single, efficient workflow
This talk introduces Multi-Aspect Verification (MAV), a method for checking several program properties simultaneously within a single verification run.
By sharing intermediate results across aspects, the MAV implementation significantly reduces redundant work, achieving up to a 5× speedup compared to a basic single-aspect approach, while changing verification outcomes in only about 2% of cases.
The presentation focuses on practical experience with MAV in the context of Linux driver verification.