Maxwell Levatich

Research interests

I have no active research projects currently, but I'm excited about the challenges and opportunities facing computer science education as a result of generative AI.

My research goal during my PhD was to develop scalable, static dataflow analyses for C programs that don't sacrifice soundness even in the face of undecidable pointer analysis. I took inspiration from iterative, constraint-based techniques in symbolic model checking and program verification, my initial area of study.

My thesis applies these scalable algorithms to secure application compartmentalization by precisely tracking how sensitive data moves through a program's pointer dependencies.

Publications

• Levatich, M., & Edwards, S. A. (April 2026). Fast, Flow-Sensitive C Program Partitioning via Iterative Value-Flow Refinement. In International Conference on Software Engineering (ICSE).

• Levatich, M., Brotzman, R., Flin, B., Chen, T., Krishnan, R., & Edwards, S. A. (2022, November). C Program Partitioning with Fine-Grained Security Constraints and Post-Partition Verification. In IEEE Military Communications Conference (MILCOM).

• Bjørner, N., Levatich, M., Lopes, N. P., Rybalchenko, A., & Vuppalapati, C. (2021, June). Supercharging plant configurations using Z3. In International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR).

• Levatich, M., Bjørner, N., Piskac, R., & Shoham, S. (2020, January). Solving LIA* using approximations. In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI).

Selected talks

• Solving LIA* Using Approximations (VMCAI 2020)