Auto-Active Verification of Software with Timers and Clocks
October 2016 • Poster
Formally verify STACs at the source code level using deductive (aka auto-active) verification
Software Engineering Institute
Why Verify Source Code?
Push assurance closer to executable level
• Use verified compilers (e.g., CompCERT) to close the final gap
Don’t need to sacrifice performance
• This is a problem when we verify models
• And is a no-go for low-level system software
Easier to integrate with existing systems
• Linux kernel module means anyone using Linux can use it
• Can be modified to work with other OSes, such as SEL4
• What You Verify Is What You Execute!