Stephanie Balzer Assistant Professor Website Office 9004 Gates and Hillman Centers Email balzers@cs.cmu.edu Department Computer Science Department Administrative Support Person Oliver Moss Research Interests Programming Languages Pure and Applied Logic Software Verification Type Theory Security Security and Privacy Advisees Zak Kent Yue Yao Tesla Zhang CSD Courses Taught 15652 - Spring, 2024 15312 - Spring, 2024 15150 - Fall, 2024 The goal of my research is to enable the construction of failure-free software, software that is correct by design and secure to run. In pursuit of this goal, I am deploying rigorous reasoning methods, such as type systems and verification logics, which allow statement of the desired properties and a formal proof of their adherence. To ensure scalability, I use compositional methods, guaranteeing that individually verified parts compose to a verifiable whole. To ensure practicality, I consider verification needs arising from real-world problems. Tangible results of my research include not only formal models with correctness proofs but also software artifacts. A driving force underlying my research is the recognition that powerful and elegant solutions are fundamentally based on simple ideas, ideas that can be conveyed to and appreciated by non-experts. As such it is the aim of my research program to contribute verification tools and systems that can be used by educated practitioners, encouraging adoption of formal methods in practice.
