I'm a Senior Security Scientist at Baidu USA. Before joining Baidu, 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.
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]