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 research interest is to facilitate correct-by-construction software development while it turns out that my previous work is centered around fixing inevitable errors introduced by programming languages like C/C++. I did some work on reasoning about program approximation, especially techniques leveraging 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]
  • ct-fuzz: Fuzzing for Timing Leaks. Shaobo He, Michael Emmi, Gabriela Ciocarlie. CoRR abs/1904.07280.
  • Human Bug Finder