Temporal Safety Checking via Typestate Analysis

PhD Qualifying Examination


Title: "Temporal Safety Checking via Typestate Analysis"

by

Mr. Shuhao FU


Abstract:

Typestate analysis extends conventional type systems to enforce temporal 
safety properties by tracking object lifecycle states, typically modeled as 
finite-state machines, thereby verifying that operations occur in correct 
sequential order. Despite significant advances in static analysis for spatial 
properties such as memory safety, ensuring temporal correctness remains 
challenging due to aliasing, path explosion, and specification acquisition 
difficulties. This survey provides a comprehensive review of nearly four 
decades of research on typestate analysis, structured around three central 
pillars: (1) Specification Mining, encompassing statistical trace-based 
inference, symbolic cross-checking, runtime enforcement, and emerging 
learning-based approaches; (2) Algorithmic Innovations, covering foundational 
path-sensitive techniques, alias-aware and sparse analyses, multi-object 
protocols, kernel-specific methods, and recent machine-learning integrations; 
and (3) Applications & Impacts, highlighting effective deployments in 
concurrency verification, OS kernel and driver safety, security protocol 
compliance, and API/error-handling correctness.


Date:                   Thursday, 4 June 2026

Time:                   2:00pm - 4:00pm

Venue:                  Room 4472
                        Lifts 25/26

Committee Members:      Prof. Charles Zhang (Supervisor)
                        Prof. Shing-Chi Cheung (Chairperson)
                        Dr. Jiasi Shen