search menu icon-carat-right cmu-wordmark

Auto-Active Verification of Software with Timers and Clocks

November 2016 Presentation
Sagar Chaki, Dionisio de Niz

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


Software Engineering Institute



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.