Lei Bu

Lei Bu is a Professor and Vice Dean of the Software Institute at Nanjing University, China. He has been with Nanjing University since 2010, progressing from Assistant Professor to his current position. His academic career includes a visiting position at Microsoft Research Asia through their StarTrack Program from 2014-2015.

Professor Bu received his B.Sc. and Ph.D. degrees in Computer Science from Nanjing University, with additional research experience at Carnegie Mellon University and University of Texas at Dallas during his doctoral studies. His academic journey shows steady progression through the ranks at his alma mater.

Lei Bu's research primarily focuses on software verification, testing, and analysis, with particular expertise in model checking, bounded model checking, formal methods, and cyber-physical systems. His work spans theoretical foundations to practical applications in safety-critical systems. Recent publications demonstrate growing interest in integrating machine learning techniques with traditional formal methods, as seen in works like SpecGen that leverage large language models for program specification generation.

His research outputs show a consistent focus on verification techniques for complex systems, particularly addressing challenges in hybrid systems, cyber-physical systems, and IoT applications. Professor Bu has developed several verification tools including BACH (Bounded Reachability Checker for Linear Hybrid Automata) and BRICK (Bounded Reachability Checker of Numerically-Intensive C Code), which have been used in international verification competitions.

• 2023: Zhongchuang Software Talent Award
• 2022: CCF-IEEE CS Young Computer Scientist Award
• 2020: The Outstanding Teachers of Computing in Higher Education Award Program
• 2019: NASAC Young Software Innovation Award
• 2016: Young Talent Development Program
• 2014: StarTrack Program Visiting Young Faculty
• 2007: Full Scholarship under the State Scholarship Fund

Professor Bu serves as a Principal Investigator on multiple significant research projects funded by the Natural Science Foundation of China, including a Key Program grant (2023-2027) on dynamic adjustment-control-fault tolerance theory. He has also advised numerous students and taught courses including Formal Languages and Automata, Theoretical Foundation of Software Engineering, and Preliminary Introduction to the Theory of Computation. His laboratory work focuses on developing practical verification tools for industrial applications in cyber-physical and IoT systems.