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

Topics

Publication Date

Poster

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!