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!