Stephanie Balzer
Office
9004 Gates and Hillman Centers
balzers@cs.cmu.edu
Department
Computer Science Department
Administrative Support
Research Areas
Research Interests
Pure and Applied Logic
Security and Privacy
Software Verification
Type Theory
Advisees
Research Statement
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.