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 the track leader of the PDCB track of the 6th International Competition on Verifying Continuous and Hybrid Systems ARCH-COMP 2022 , 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 (微软亚洲研究院)

 

 

 
  • 09/2007, Full Scholarship under the State Scholarship Fund by the China Scholarship Council (CSC, 国家留学基金委).

[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]

Teaching:  

 

 

 

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

 

 

 

  • Theoretical Foundation of Software Engineering (24 Spring, 23 Spring, 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)

 

 

 

  • Formal Languages and Automata (24 Autumn, 23 Autuma, 22 Autumn, 21 Autumn, 20 Autumn, 15 Spring, 14 Spring, 13 Spring, 12 Spring, 11 Spring, Open to both undergraduate and graduate 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

  • (Bounded) Reachability Analysis of Linear/Nonlinear Hybrid Automata.
  • Online Modeling and Verification of Cyber-Physical Systems
  • Symbolic Execution of Complex Software Code
  • Formal Checking and Fixing of IoT System

**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 My Google Scholar Profile ; My DBLP

 

  • 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'24), 329-355.

 

 

 

  • 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'24), 3:1-3:12, 2024.

 

 

 

  • Lei Bu, Qiuping Zhang, Suwan Li, Jinglin Dai, Guangdong Bai, Kai Chen, Xuandong Li. Security Checking of Trigger-Action-Programming Smart Home Integrations, ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'23), 639-651, 2023.

 

 

 

  • 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..

 

 

 

  • Suwan Li, Lei Bu, Guangdong Bai, Zhixiu Guo, Kai Chen. VITAS : Guided Model-based VUI Testing of VPA Apps, International Conference on Automated Software Engineering (ASE 2022), 115:1-115:12, 2022.

 

 

 

  • 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, Zhunyi Xie, Lecheng Lyu, Yichao Li, Xiao Guo, Jianhua Zhao, Xuandong Li. BRICK: Path Enumeration Based Bounded Reachability Checking of C Program (Competition Contribution), 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2022), 408-412, 2022.

 

 

 

  • Yuming Wu, Lei Bu, Jiawan Wang, Xinyue Ren, Wen Xiong, Xuandong Li. Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata, 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022), 473-495, 2022.

 

 

 

  • Jiawan Wang, Lei Bu, Shaopeng Xing, Yuming Wu, Xuandong Li. Combined Online Checking and Control Synthesis: A Study on a Vehicle Platoon Testbed, 24th International Symposium on Formal Methods (FM 2021), 752-762, 2021.

 

 

 

  • 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.

 

 

 

  • Shaopeng Xing, Jiawan Wang Lei Bu, Xin Chen, and Xuandong Li. Approximate optimal hybrid control synthesis by classification-based derivative-free optimization, In Proceedings of 24th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2021), 7:1-11, 2021.

 

 

 

  • Shiyu Zhang, Juan Zhai, Lei Bu, Mingsong Chen, Linzhang Wang, Xuandong Li. Automated Generation of LTL Specifications For Smart Home IoT Using Natural Language, 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE 2020), 622-625, 2020.

 

 

 

  • 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:

 

 

 

 

[Top]

Selected Talks:  

 

 

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
   

Recent Selected Invited Talks:

  • Online Verification-Based Safety Monitoring and Control Synthesis of Real-time Cyber-Physical System, University of Science and Technology of China, July 27, 2022
   
  • Online Verification-Based Safety Monitoring and Control Synthesis of Real-time Cyber-Physical System, Peking University, June 14, 2022
   
  • Learning-enabled Symbolic Execution, Huawei Symposium of Dynamic and Static Software Analysis , March 10, Online, 2022
   
  • Online Verification-Based Safety Monitoring and Control Synthesis of Real-time Cyber-Physical System, Embedded System Symposium of CNCC 2021, Shenzhen, December 16, 2021
   
  • Learning-enabled Falsification and Optimal Control of Cyber-Physical Systems, Symposiums of ACM SIGBED China, Hefei, July 30, 2021
   
  • Learning-enabled Falsification and Optimal Control of Cyber-Physical Systems, NIO Automobile, Shanghai, July, 2021
   
  • Learning-enabled Falsification and Optimal Control of Cyber-Physical Systems, JIDU Automobile, Shanghai, July, 2021
   
  • Path-oriented Bounded Verification and Application, Young Scientist Forum, NASAC 2020, Chongqing, November, 2020
   
  • Systematically Ensuring the Confidence of Home Automation IoT Systems By Model Checking. TAV-CPS/IoT@ISSTA 2019, Beijing, July, 2019
   
  • Path-Oriented Reachability Analysis of Composed Linear Hybrid Systems under Shallow Synchronization Semantics. Trends@Concur 2018, Beijing, September, 2018
   
  • Machine Learning Driven Symbolic Execution of Complex Program. Artificial Intelligence and Trustworthy Software International Summer Session On Trustworthy Software, Shanghai, July, 2018
   
  • Automatically Verifying the Confidence of Home Automation IoT Systems. Purdue University, April, 2017
   

[Top]
Fundings:  

 

 

Ongoing Projects:

 

  • 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))

 

 

 

  • Principle Investigator, Runtime Evolution and Trustworthy Assurance of Intelligent Software Under Nondeterministic Environment. (2020-2025, Leading-edge Technology Program of Jiangsu Natural Science Foundation)

 

 

 

  • Principle Investigator, Path Enumeration Based Software Bounded Model Checking Techniques and System.(2022-2025, Natural Science Foundation of China (General Program))

 

 

Completed Projects:

 

  • Principle Investigator, Complex Behavioral Scenario Oriented Model Checking Techniques For Real Time and Hybrid Systems.(2016-2019, Natural Science Foundation of China (General Program))

 

 

 

  • Principle Investigator, Runtime Measuring and Checking of Cyber Physical Systems.(2015-2018, NSFC-ISF Joint Project, Israel PI: Prof. Doron A. Peled)

 

 

 

  • Principle Investigator, Model Checking Techniques and Application For Hybrid System.(2012-2014, Natural Science Foundation of China (Youth Program))

 

 

 

  • Principle Investigator, Formal Verification Techniques For Cyber-Physical System.(2012-2014, JiangSu Natural Science Foundation)

 

 

[Top]

   
 

 

Last Updated September, 2024