Formally Correct Intermittent Systems

This lecture by the instructor focuses on designing formally correct intermittent systems, addressing the challenges of ensuring correctness in batteryless systems powered intermittently. The lecture covers the lack of correctness definitions in existing systems, obstacles to correctness guarantees, and the research strategy employed to identify fundamental correctness conditions. It delves into the formal model overview, the importance of memory consistency, and the need for enforcing constraints simply without concrete-time reasoning. The lecture also discusses the implications of unchecked assumptions in current systems, the development of a type system approach for safe intermittence, and the importance of security and full-stack reasoning for extreme edge devices.