icon-carat-right menu search cmu-wordmark

Auto-Active Verification of Software with Timers and Clocks

Presentation
Software that accesses the system clock is the key to real-time and cyber-physical systems
Publisher

Software Engineering Institute

Watch

Abstract

The goal of this work is to formally verify software with timers and clocks (STACs) at the source code level using deductive (also known as auto-active) verification. Our target is the ZRSM mixed-criticality scheduler.