As IoT devices become increasingly prevalent, embedded systems operating in resource-constrained environments must carefully account for their energy requirements. These requirements are typically expressed as the \textit{worst-case energy consumption} (WCEC), the maximum possible energy consumed across any possible execution. A common approach to obtaining this bound is through static analysis techniques that reason over all possible program executions.

However, the stateful nature of peripherals is a particular obstacle for static analysis. Existing static analyses are insufficient in two key ways: (1) peripherals are either unmodeled or modeled under overly restrictive assumptions, limiting applicability to a narrow class of devices and programs; and (2) existing tools impose significant workflow burden, requiring external tool integration or custom peripheral implementations from the programmer.

To address these limitations, we utilize \textit{typestate}, for peripherals by encoding a type-level representation of a peripheral’s modes of operation and combine it with prior work on automatic cost analysis in type systems. The result is, to our knowledge, the first type system to unify these two ideas, enabling symbolic energy bounds for embedded systems without invasive changes to programmer workflow.

I am an intern with the Trustworthy Systems group at University of New South Wales in Sydney, Australia and a rising senior at the University of Maryland. My research interests lie in the intersection of programming languages, formal methods, and systems.