Cedar Breaks National Monument Shaobo He
School of Computing
University of Utah

I'm a fifth year computer science PhD student in School of Computing, University of Utah. I'm lucky to be advised by Prof. Zvonimir Rakamaric.


My current research interest is to reason about program approximation, especially techniques leveraging low-bitwidth floating-point representations. I am also a contributor to SMACK (adding support for bit-vectors, Rust, floating-point, etc.). To find more about my research and other exciting projects, please visit SOARlab.


  • Towards Automated Differential Program Verification For Approximate Computing. Shaobo He. Student Forum at the 15th Conference on Formal Methods in Computer-Aided Design (FMCAD 2015), Austin, Texas, USA. [poster]
  • SMACK Software Verification Toolchain. Montgomery Carter, Shaobo He, Jonathan Whitaker, Zvonimir Rakamaric, Michael Emmi. Demonstrations Track at the 38th IEEE/ACM International Conference on Software Engineering (ICSE 2016), Austin, TX, USA. [link]
  • Verifying Relative Safety, Accuracy, and Termination for Program Approximations. Shaobo He, Shuvendu K. Lahiri, Zvonimir Rakamaric. 8th NASA Formal Methods Symposium (NFM 2016), Minneapolis, MN, USA. [link]
  • Counterexample-Guided Bit-Precision Selection. Shaobo He, Zvonimir Rakamaric. 15th Asian Symposium on Programming Languages and Systems (APLAS 2017), Suzhou, China.[link]
  • Verifying Rust Programs with SMACK. Marek Baranowski, Shaobo He, Zvonimir Rakamaric. 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), Los Angeles, CA, USA. [link]
  • Links

    SOARlab reading group