Semantics-Based WCET Analysis

This dissertation presents the design of a definitional semantics-based WCET analyzer, bridging the gap between the  principles of formal executable specification, promoted by the K  framework and the existing methods and techniques, which were successfully applied in analysis and verification of embedded software.