Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type


Publication Date


Auto-Active Verification of Software with Timers and Clocks

  • October 2016
  • By Sagar Chaki
  • Formally verify STACs at the source code level using deductive (aka auto-active) verification
  • Publisher: Software Engineering Institute
  • Abstract

    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!