Lei Bu

Professor, PH.D.

Vice Dean of Software Institute,

Nanjing University,

Room 308, Computer Science Building, Xianlin Campus, Nanjing University, Nanjing, Jiangsu, 210023, P.R.China
Tel/Fax: 86-25-89680916

Email: bulei at nju.edu.cn

[News]

[Short Biography]

[Work Experience]

[Selected Awards]

[Education]

[Teaching]

[Research Interest]

[Selected Publication]

[Selected Tools]

[Selected Talks ]

[Fundings]

News:

• I am one of the Program Co-chairs of CCF ChinaSoft 2026, please join this event.

• I am one of the Program Co-chairs of ATVA 2026, please join this event.

• I am one of the General Co-chairs of Internetware 2026, please join this event.

• I am the track leader of the PCDB track of International Competition on Verifying Continuous and Hybrid Systems ARCH-COMP , please join us and have fun.

[Top]

Short Biography:

I am a Professor in the Software Engineering Group led by Prof. Xuandong Li in Nanjing University.

I received my B. Sc. and Ph. D. degrees in computer science from Department of Computer Science and Technology, Nanjing University, China, in 2004 and 2010, respectively. I joined Department of Computer Science and Technology of Nanjing University in 2010 as an assistant professor.

My research areas include but not limited to: Model Checking, Bounded Model Checking, Formal Methods, Real time and Hybrid System, Cyber Physical System, Software Testing, Software Analysis, Dependable System and Software Engineering

[Top]

Work Experience:

• 07/2022-Present, Professor, Vice Dean, Software Institute, Nanjing University, Nanjing, Jiangsu, P.R.China.

• 12/2018-06/2022, Professor, Department of Computer Science and Technology, Nanjing University, Nanjing, Jiangsu, P.R.China.

• 12/2013-12/2018, Associate Professor, Department of Computer Science and Technology, Nanjing University, Nanjing, Jiangsu, P.R.China.

• 09/2014-03/2015, StarTrack Program Visiting Young Faculty, Software Analytics Group, Microsoft Research Asia, Beijing, P.R.China.

• 08/2010-12/2013, Assistant Professor, Department of Computer Science and Technology, Nanjing University, Nanjing, Jiangsu, P.R.China.

[Top]

Selected Awards:

• 10/2023, Zhongchuang Software Talent Award(中创软件人才奖), by Zhongchuang Software Fundation(中创软件基金)

• 10/2022, CCF-IEEE CS Yound Computer Scientist Award (CCF青年科技奖/CCF-IEEE CS青年科学家奖), by China Computer Federation (中国计算机学会), IEEE Computer Society

• 12/2020, The Outstanding Teachers of Computing in Higher Education Award Program (高校计算机优秀教师奖励计划), by The National Computing Teaching Advisory Board under Ministry of Education(教育部高等公司计算机类专业教学指导委员会), China Computer Federation (中国计算机学会), China Teacher Development Foundation(中国教师发展基金会)

• 11/2019, NASAC Young Software Innovation Award (NASAC青年软件创新奖), by Software Engineering Technical Committee (软件工程专委) and System Software Technical Committee(系统软件专委), China Computer Federation (中国计算机学会)

• 01/2016, Young Talent Development Program (青年人才发展计划), by China Computer Federation (中国计算机学会)

• 09/2014, StarTrack Program Visiting Young Faculty (铸星计划), by Microsoft Research Asia (微软亚洲研究院)

[Top]

Education:

• 09/2006-04/2010, Candidate for Doctoral degree in Computer Software and Theory, Department of Computer Science and Technology, Nanjing University, Nanjing, Jiangsu, P.R.China. Supervisor: Prof. Xuandong Li.

• 09/2007-09/2008, Visiting Student in Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA. Supervisor: Prof. Edmund M. Clarke.

• 02/2006-09/2006, Visiting Student in Department of Computer Science, University of Texas at Dallas, Richardson, TX, USA. Supervisor: Prof. W. Eric Wong.

• 09/2004-07/2006, Candidate for Master degree in Computer Software and Theory, Department of Computer Science & Technology, Nanjing University, Nanjing, Jiangsu, P.R.China. Supervisor: Prof. Xuandong Li.

• 09/2000-06/2004, Bachelor degree in Computer Science and Technology, Department of Computer Science & Technology, Nanjing University, Nanjing, Jiangsu, P.R.China. Supervisor: Prof. Xuandong Li.

[Top]

• Formal Languages and Automata (26 Autumn, 25 Autumn, 24 Autumn, 23 Autumn, 22 Autumn, 21 Autumn, 20 Autumn, 15 Spring, 14 Spring, 13 Spring, 12 Spring, 11 Spring, Open to both undergraduate and graduate students)

• Theoretical Foundation of Software Engineering (26 Spring, 25 Spring, 24 Spring, 23 Spring, Open to both undergraduate and graduate students)

• Preliminary Introduction to the Theory of Computation (19 Autumn, 18 Autumn, 17 Autumn, 16 Autumn, 15 Autumn, Open to both undergraduate and graduate students)

• Practice of Fundamental Programming (22 Spring (Advanced Programming), 21 Spring, 20 Spring, 19 Spring, 18 Spring, 17 Spring, 16 Spring, 15 Spring, Open to undergraduate students)

• JAVA Programming Language (14 Spring, 13 Spring, 12 Spring, 11 Spring, undergraduate course for Extension School)

• Network Application and Technology (12 Fall, 11 Fall, 10 Fall, undergraduate course for Extension School)

[Top]

Research Interest:

My current research interests are mainly in the areas of

• Trustworthy Construction and Assurance of Cyber-Physical Systems and Embodied AI.

• LLM-empowered Formal Verification of Large Scale Software.

• Model-based Analysis of Software Security.

**In general, I am recruiting well motivated and dedicated Ph.D. / master students to do research in above-mentioned areas. Undergraduate students are also encouraged to contact me, to work on related topics.

[Top]

Recent Selected Publications:

Full list please refer to My Google Scholar Profile

• Suwan Li, Lei Bu, Shangqing Liu, Guangdong Bai, Fuman Xie, Kai Chen, Chang Yue.VUI Testing of VPA Apps via Behavior Model-Enhanced LLM Agents, ACM Transactions on Software Engineering and Methodology (TOSEM), 35(7)，1-34，2026.

• Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, Lei Bu. SpecGen: Automated generation of formal program specifications via large language models, 47th IEEE/ACM International Conference on Software Engineering, (ICSE 2025), 16-28, 2025.

• Yuhui Shi, Yuming Wu, Lei Bu, Xuandong Li. Checking Bounded Reachability of Compositional Linear Hybrid Automata Using Interaction Relations. International Conference on Embedded Software, (EMSOFT 2025), published in ACM Transactions on Embedded Computing Systems (TECS), 2025.

• Jiawan Wang, Wenxia Liu, Muzimiao Zhang, Jiaqi Wei, Yuhui Shi, Lei Bu, Xuandong Li. Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs, International Conference on Computer Aided Verification (CAV 2024), 329-355, 2024.

• Xiao Guo, Jianhua Zhao, Lei Bu. Poles-based Invariant Generation for Verifying the BIBO Stability of Digital Filters, ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2024), 3:1-3:12, 2024.

• Limin Wang, Lei Bu, Fu Song. SCAGuard: Detection and Classification of Cache Side-Channel Attacks via Attack Behavior Modeling and Similarity Comparison, Design Automation Conference 2023 (DAC 2023), 1-6, 2023.

• Xizao Wang, Zhiqiang Zuo, Lei Bu, Jianhua Zhao. DStream: A Streaming-Based Highly Parallel IFDS Framework, International Conference on Software Engineering (ICSE 2023), 2488-2500, 2023.

• Jiawan Wang, Lei Bu, Shaopeng Xing, Xuandong Li. PDF: Path-Oriented, Derivative-Free Approach for Safety Falsification of Nonlinear and Nondeterministic CPS, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 41(2): 238-251, 2022.

• Lei Bu, Zhe Zhao, Yuchao Duan, Fu Song. Taking Care of the Discretization Problem: A Comprehensive Study of the Discretization Problem and a Black-box Adversarial Attack in Discrete Integer Domain, IEEE Transactions on Dependable and Secure Computing (TDSC), 2021.

• Lei Bu, Yongjuan Liang, Zhunyi Xie, Hong Qian, Yi-Qi Hu, Yang Yu, Xin Chen, Xuandong Li. Machine Learning Steered Symbolic Execution Framework for Complex Software Code, Formal Aspects of Computing (FAOC), 33(3): 301-323, 2021.

• Lei Bu, Qixin Wang, Xinyue Ren, Shaopeng Xing, Xuandong Li. Scenario-Based Online Reachability Validation for CPS Fault Prediction, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 39(10): 2081-2094, 2020.

[Top]

Tools:

• BACH Toolset: Bounded Reachability Checker For Linear Hybrid Automata, CPS System

• MLB: Machine Learning Based Symbolic Execution For JAVA

• BRICK: Bounded Reachability Checker of Numerically-Intensive C Code [A new version of BRICK which supports UBUNTU 20 is available here.]

[Top]

Tutorial:

• Formal Analysis, Verification and Design of Safety-Critical CPS, RTSS 2020

• BACH: From Bounded Reachability Analysis of Linear Hybrid Automata To Online Verification of Industrial Cyber-Physical System. Half-day tutorial, FM 2014, Singapore, May, 2014

Lecture:

• Path-oriented Bounded Verification of Complex Software, August 9, 2022, System Security Summer School, Zhejiang University，Online

• BACH: Path-oriented Reachability Checker of Linear Hybrid Automata, July, 2020, National University of Defense Technology，Online

• From Bounded Reachability Analysis of Linear Hybrid Automata To Verification of Industrial CPS and IoT, The 5th School on Engineering Trustworthy Software Systems (SETSS19), April 21-27, 2019, Southwest University, Chongqing China

• Verification of Linear Hybrid Automata for Liveness, Carnegie Mellon University, Pittsburgh, USA, April, 2008

[Top]

• Principle Investigator, Trustworthy Construction and Assurance of Real Time Hybrid Systems. (2027-2031, Natural Science Foundation of China (Young Scientists Fund-A))

• Principle Investigator, Dynamic Adjustment-Control-Fault Tolerance Theory and Implementation Methods For the Behavior of Software Working in Open and Nondeterministic Scenarios. (2023-2027, Natural Science Foundation of China (Key Program))

[Top]