Cedar Breaks National Monument Shaobo He (何少博)

I was a postdoctoral research associate at School of Computing, University of Utah, where I also obtained my PhD. I was 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] [repo]
  • 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]
  • Stochastic Local Search for Solving Floating-Point Constraints. Shaobo He, Marek Baranowski, Zvonimir Rakamaric. 12th International Workshop on Numerical Software Verification (NSV 2019), New York, NY, USA.[link][repo]
  • Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification. Jack Garzella, Marek Baranowski, Shaobo He, Zvonimir Rakamaric. 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2020), New Orleans, LA, USA.[link]
  • An SMT Theory of Fixed-Point Arithmetic. Marek Baranowski, Shaobo He, Mathias Lechner, Thanh Son Nguyen, Zvonimir Rakamaric. 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France. [link]
  • ct-fuzz: Fuzzing for Timing Leaks. Shaobo He, Michael Emmi, Gabriela Ciocarlie. Testing Tools Track at the 13th International Conference on Software Testing, Verification and Validation (ICST 2020), Porto, Portugal.[link] [repo]