I'm a second year MS student advised by Prof. Grigore Rosu. My research interests are focused around formal methods theory and its application to improve software quality, robustness, and security. I'm particularly interested in the application of formal methods to the blockchain paradigm. Currently, I'm working on the K Semantics of the EVM (KEVM), and the K Framework's language independent debugging capabilities.
- 2016 - Present - M.S. C.S. University of Illinois, Urbana Champaign
- 2015 - 2016 - Software Developer, Runtime Verification Inc.
- 2015 - B.S. C.S. University of Illinois, Urbana Champaign
- Programming Language Semantics, Static and Dynamic Analysis, Language Independent Formal Verification and Debugging.
- Software Robustness, Safety and Security.
- Practical Software Tools with rigorous theoretical backgrounds.
- Hildenbrandt E., Saxena M., Zhu, X., Rodrigues N., Daian P., Guth D., Roşu G. (2017) KEVM: A Complete Semantics of the Ethereum Virtual Machine (Technical Report), http://hdl.handle.net/2142/97207
- Guth D., Hathhorn C., Saxena M., Roşu G. (2016) RV-Match: Practical Semantics-Based Program Analysis. In: Chaudhuri S., Farzan A. (eds) Computer Aided Verification. CAV 2016. Lecture Notes in Computer Science, vol 9779. Springer
- Daian P, Guth D., Hathhorn C., Li, Y., Pek, E., Saxena M., Serbanuta, T,. Rosu, G. (2016) Runtime Verification at Work: A Tutorial. In: Falcone Y., Sánchez C. (eds) Runtime Verification. RV 2016. Lecture Notes in Computer Science, vol 10012. Springer, Cham
- 2107 Thomas M. Siebel Center for Computer Science, 201 N. Goodwin Avenue, Urbana, IL 61801
- msaxena2 AT illinois DOT edu
- I'm an amateur guitarist, and like blues and blues rock. My favorite guitarists are B.B. King, Eric Clapton, and Slash. I plan to, at some point, formalize the theory of blues in K (Given a sequence of notes, prove whether it'll sound good or not).
- I'm an open source enthusiast. You can usually find whatever I'm working on at my Github Profile.