Our verification framework CSL-Style refinement-Based Contextual Relational P1 rogram logic Refine Assertion Entailment B Refinement-Based Verification Verification Condition High-LevelLanguage High-Level Operational Semantics Generator with Configurable Schedulers Domain High-Level Specifi Assembly C Subset Spec Language Primitives Solvers A Modeling of Low-Level Operational Semantics C Co with Context Switch and Interrupts OS Kernels Tactics Low-Levellanguage Refinement-Based Verification Framework
Our Verification Framework High-Level Spec. Language C Subset Assembly Primitives Low-Level Operational Semantics with Context Switch and Interrupts High-Level Operational Semantics with Configurable Schedulers High-Level Language Low-Level Language CSL-Style Refinement-Based Program Logic Contextual Refinement B. Refinement-Based Verification Refinement-Based Verification Framework A. Modeling of C. Coq OS Kernels Tactics Relational Assertion Entailment Verification Condition Generator DomainSpecific Solvers …
Program Logic for Refinement and Multi-Level Interrupts Relational program logic for proving simulation relation Ownership-Transfer semantics for reasoning about multi-level interrupts Combining above two for our CSL-Style relational program logic
Program Logic for Refinement and Multi-Level Interrupts • Relational program logic for proving simulation relation • Ownership-Transfer semantics for reasoning about multi-level interrupts • Combining above two for our CSL-Style relational program logic