search menu icon-carat-right cmu-wordmark

Auto-Active Verification of Software with Timers and Clocks

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!