Research interests
My research is on developing scalable, static dataflow analyses for C programs that don't sacrifice soundness even in the face of undecidable pointer analysis. I take inspiration from iterative, constraint-based techniques in symbolic model checking and program verification, my initial area of study. I am also fond of SMT solvers, and I find ways to leverage their power to tackle the difficult kernels of my algorithms.
My recent work applies these scalable algorithms to secure application compartmentalization by precisely tracking how sensitive data moves through a program's pointer dependencies.
Publications
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 MILCOM 2022-2022 IEEE Military Communications Conference (MILCOM) (pp. 285-291). IEEE.
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 (pp. 1-25). Cham: Springer International Publishing.
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 (pp. 360-378). Cham: Springer International Publishing.
Selected talks
Solving LIA* Using Approximations (Presented at VMCAI 2020)