Huanhuan Sheng

alt text 

Huanhuan Sheng
Master's Student at Institute of Software, Chinese Academy of Sciences
Beijing, China

Email: shenghh@ios.ac.cn

About me

I am a Master's student in computer science at Institute of Software, Chinese Academy of Sciences, under the guidance of Dr. Bohua Zhan. I am in the research group in State Key Lab. of Computer Science leaded by Prof. Naijun Zhan. My research focused on theorem proving of hybrid systems. And I am going to work on safe reinforcement learning via formal methods.

Education

  • M.Eng. in Computer Science, University of Chinese Academy of Sciences (UCAS), Sep. 2020 (- July 2023)

  • B.Eng. in Materials Science and Engineering, Zhejiang University (ZJU), Sep. 2016 - July 2020

Experiences

Research Experiences

  • HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic
    Research Assistant, Master's Thesis Research

    • Designed and proved rules for ordinary differential equation commands in Hybrid Communicating Sequential Processes.

    • Devised verification condition generation algorithm with Python implementation.

    • Designed labelling and highlighting mechanisms to distinguish and visualize verification conditions for proof reuse and debugging purposes.

    • Developed a user-friendly interface for the tool, implemented in JavaScript.
      HHLPy is also part of the Mars toolchain and has already been used successfully in other projects..

  • Requirements Classification and Formalization of Trustworthy Systems
    Group Member, Industrial Collaboration with Huawei Technologies Co., Ltd.

    • Searched and summarized recent works on formal specification and verification tools on security and privacy.

    • Presented trustworthiness-related papers in weekly seminar with Huawei.

Course Projects

  • Deep Learning, Reinforcement Learning: Completed projects such as sentiment analysis of movie comments, automatic poem writing, cats vs dogs classification, cart pole control, gridworld, etc.

  • Foundation of Network Attack and Defense: Implemented a Network Sniffer, Ran a Buffer Overflow Attack on War-ftp 1.65.

  • Concurrent Data Structures and Multicore Programming: Built a Train Ticketing System.

Publications

Accepted

  • Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan. HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic. FM 2023.

  • Stefan Mitsch, Bohua Zhan, Huanhuan Sheng, Alexander Bentkamp, Xiangyu Jin, Shuling Wang, Simon Foster, Christian Pardillo Laursen, Jonathan Julian Huerta y Munive. ARCH-COMP22 Category Report: Hybrid Systems Theorem Proving. ARCH 2022, https://easychair.org/publications/paper/JB8Q

  • Shuling Wang, Bohua Zhan, Huanhuan Sheng, Hao Wu, Shicheng Yi, Lingtai Wang, Xiangyu Jin, Bai Xue, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao. Survey on Requirements Classification and Formalization of Trustworthy Systems. Journal of Software, 33(7):2367–2410, 2022, http://www.jos.org.cn/josen/article/abstract/6587 (in Chinese).

Under review

  • Ehsan Ahmad, Xiong Xu, Huanhuan Sheng, Bohua Zhan, Naijun Zhan. Modelling and Verification of Hybrid Systems by Extending AADL. TOSEM.

Key Skills

Python, C, JavaScript, Pytorch, Vue.

Honors

  • 2nd-class Academic Scholarship, 2021 & 2022

  • Outstanding Graduates of Zhejiang University, 2020

  • 1st-class Scholarship for Excellence in Research and Innovation, 2019

  • Zhejiang Government Scholarship, 2017 & 2018

  • 2nd-class Scholarship for Outstanding Students, 2017 & 2018, etc