Batteryless, energy-harvesting devices (EHDs) are a new class of embedded  computing platform that are powered solely by energy collected from the  environment, without using batteries. These devices enable new applications in  domains like disaster monitoring, body implants, or smart city infrastructure.  Unfortunately, environmental energy is scarce, so EHDs are powered only  intermittently, experiencing frequent failures that make correct programming  difficult. The field of intermittent computing seeks to overcome the correctness  and programmability challenges introduced by these power failures but has  historically relied on ad-hoc correctness reasoning that provides no guarantees,  limiting the effectiveness of EHDs as many of the envisioned application  domains have high assurance requirements. 

This talk presents my research in leveraging formal methods and programming language techniques to design systems for EHDs that have provable correctness guarantees. I will cover the basics of intermittent computing; my recent work in designing formally correct intermittent systems for sequential, single-node platforms; and my ongoing work in supporting more complex, concurrent platforms.

Throughout, I will highlight the importance of modularity and abstraction in both formalism and system design and how that connects to my end goal of creating full-stack verification pipelines for emerging computing platforms.