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 Rakamarić.
Research
My research interest is to facilitate correct-by-construction software
development while it turns out that my previous work was mostly about fixing
inevitable errors introduced by programming languages like C/C++.
I did some work on reasoning about program approximation, especially
techniques leveraging floating-point or fixed-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.
Publication
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]
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, Andrew M. Wells. Proceedings of the ACM on Programming Languages, Volume 8, Issue OOPSLA1.
[link][repo]
How We Built Cedar: A Verification-Guided Approach. Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, Andrew Wells. FSE 2024: Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering.
[link][extended version][repo]
