Manasvi Saxena

From FSL
Revision as of 07:11, 14 December 2017 by Msaxena2 (Talk | contribs)

Jump to: navigation, search



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.

Short Biography

  • 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

Research Interests

  • Programming Language Semantics, Static and Dynamic Analysis, Language Independent Formal Verification and Debugging.
  • Software Robustness, Safety and Security. I'm particularly interested in applications of Formal Methods in Blockchain based systems.
  • 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),
  • 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.
Personal tools