Shaobo He何少博

Shaobo He

I was a postdoctoral research associate at the School of Computing, University of Utah, where I also obtained my PhD. I was lucky to be advised by Zvonimir Rakamarić.

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, and more. To find out about my research and other exciting projects, please visit SOAR Lab.

Publications

  1. 2024 FSE

    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

    paper extended repo

  2. 2024 OOPSLA

    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

    paper repo

  3. 2020 ICST

    ct-fuzz: Fuzzing for Timing Leaks

    Shaobo He, Michael Emmi, Gabriela Ciocarlie · Testing Tools Track

    paper repo

  4. 2020 IJCAR

    An SMT Theory of Fixed-Point Arithmetic

    Marek Baranowski, Shaobo He, Mathias Lechner, Thanh Son Nguyen, Zvonimir Rakamarić

    paper

  5. 2020 VMCAI

    Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification

    Jack Garzella, Marek Baranowski, Shaobo He, Zvonimir Rakamarić

    paper

  6. 2019 NSV

    Stochastic Local Search for Solving Floating-Point Constraints

    Shaobo He, Marek Baranowski, Zvonimir Rakamarić

    paper repo

  7. 2018 ATVA

    Verifying Rust Programs with SMACK

    Marek Baranowski, Shaobo He, Zvonimir Rakamarić

    paper

  8. 2017 APLAS

    Counterexample-Guided Bit-Precision Selection

    Shaobo He, Zvonimir Rakamarić

    paper repo

  9. 2016 NFM

    Verifying Relative Safety, Accuracy, and Termination for Program Approximations

    Shaobo He, Shuvendu K. Lahiri, Zvonimir Rakamarić

    paper

  10. 2016 ICSE

    SMACK Software Verification Toolchain

    Montgomery Carter, Shaobo He, Jonathan Whitaker, Zvonimir Rakamarić, Michael Emmi · Demonstrations Track

    paper

  11. 2015 FMCAD

    Towards Automated Differential Program Verification for Approximate Computing

    Shaobo He · Student Forum

    poster

Writing