BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Designing Formally Correct Intermittent Systems
DTSTART:20230313T100000
DTEND:20230313T110000
DTSTAMP:20260406T171931Z
UID:1afcd58d387cd36de515b6b650a5f5c54d15d414b8ba13583b32b3cc
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Milijana Surbatovic - Carnegie Mellon University\nIC Facul
 ty candidate\n\nAbstract\n"Extreme edge computing" is an emerging computin
 g paradigm targeting application domains like medical wearables\, disaster
 -monitoring tiny satellites\, or smart infrastructure. This paradigm bring
 s sophisticated sensing and data processing into an embedded device's depl
 oyment environment\, enabling computing in environments that are too harsh
 \, inaccessible\, or dense to support frequent communication with a centra
 l server. Batteryless\, energy harvesting devices (EHDs) are key to enabli
 ng extreme edge computing\; instead of using batteries\, which may be too 
 costly or even impossible to replace\, they can operate solely off energy 
 collected from their environment. However\, harvested energy is typically 
 too weak to power a device continuously\, causing frequent\, arbitrary pow
 er failures that break traditional software and make correct programming d
 ifficult. Given the high assurance requirements of the envisioned applicat
 ion domains\, EHDs must execute software without bugs that could render th
 e device inoperable or leak sensitive information. While researchers have 
 developed intermittent systems to support programming EHDs\, they rely on 
 informal\, undefined correctness notions that preclude proving such necess
 ary correctness and security properties.\n\nMy research lays the foundatio
 n for designing formally correct intermittent systems that provide correct
 ness guarantees. In this talk\, I show how\nexisting correctness notions a
 re insufficient\, leading to unaddressed bugs. I then present the first fo
 rmal model of intermittent execution\, along with correctness definitions 
 for important memory consistency and timing properties. I use these defini
 tions to design and implement both the language abstractions that programm
 ers can use to specify their desired properties and the enforcement mechan
 isms that uphold them. Finally\, I discuss\nmy future research directions 
 in intermittent system security and leveraging formal methods for full-sta
 ck correctness reasoning.\n\nBio\nMilijana Surbatovich is a PhD Candidate 
 in the Electrical and Computer Engineering Department at Carnegie Mellon U
 niversity\, co-advised by Professors\nBrandon Lucia and Limin Jia. Her res
 earch interests are in applied formal methods\, programming languages\, an
 d systems for intermittent computing and\nnon-traditional computing platfo
 rms broadly. She is excited by research problems that require reasoning ab
 out correctness and security across the\narchitecture\, system\, and langu
 age stack. She was awarded CMU's CyLab Presidential Fellowship in 2021 and
  was selected as a 2022 Rising Star in EECS. Previously\, she received an 
 MS in ECE from CMU in 2020 and a BS in Computer Science from the Universit
 y of Rochester in 2017.\n\nMore information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420 https://epfl.zoom.us/
 j/68485400529
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR