开设课程

《Preliminary Introduction to the Theory of Computation 》

《Practice of Fundamental Programming 》

《Formal Languages and Automata 》

《JAVA Programming Language 》

《Network Application and Technology》

科研项目

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

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)

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

Participator, Design and Implementation Techniques for Cyber-Physical System (2011-2013, National 863 program of China)

Participator, Techniques and Tools for Trustworthy Evaluation of Internetware (2012-2014, National 863 program of China)

Participator, Production Line Supporting Software Trustworthy Analysis and Evaluation (2007-2010, National 863 program of China)

Participator, Key Techniques and Tools For Model-Driven Software Testing and Verification(2009-2011, National 863 program of China)

Participator, Model-Based Embedded System Testing and Application on Domestic Train Control System(2011, Natural Science Foundation of China)

科研成果

论文：

Lei Bu, Qixin Wang, Xinyue Ren, Shaopeng Xing and Xuandong Li. Scenario-based Online Reachability Validation For CPS Fault Prediction, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, To Appear.

Lei Bu, Shaopeng Xing, Xinyue Ren, Yang Yang, Qixin Wang, and Xuandong Li. Incremental Online Verification of Dynamic Cyber-Physical Systems, In Proceedings of Design, Automation & Test in Europe Conference & Exhibition (DATE), pp.782-787, IEEE, 2019.

Lei Bu, Wen Xiong, Chieh-Jan Mike Liang, Shi Han, Dongmei Zhang, Shan Lin, and Xuandong Li. Systematically Ensuring The Confidence of Real Time Home Automation IoT Systems, ACM Transactions on Cyber-Physical Systems, 2(3): 22:1-22:23, 2018.

Dingbao Xie, Wen Xiong, Lei Bu, Xuandong Li. Deriving Unbounded Reachability Proof of Linear Hybrid Automata During Bounded Checking Procedure, IEEE Transactions on Computers, 66(3): 416-430, 2017.

Xin Li, Yongjuan Liang, Hong Qian, Yi-Qi Hu, Lei Bu, Yang Yu, Xin Chen, and Xuandong Li. Symbolic Execution of Complex Program Driven by Machine Learning Based Constraint Solving, In Proceedings of 31st IEEE/ACM International Conference on Automated Software Engineering (ASE), 2016.

Dingbao Xie, Lei Bu, Xuandong Li. Deriving Unbounded Proof of Linear Hybrid Automata From Bounded Verification, In Proceedings of Real-Time Systems Symposium (RTSS), pp.128-137, IEEE, 2014.

Dingbao Xie, Lei Bu, Jianhua Zhao, Xuandong Li. SAT-LP-IIS Joint-directed Path-Oriented Bounded Reachability Analysis of Linear Hybrid Automata, In Formal Methods in System Design 45 (1), 42-62, 2014.

Tao Li, Feng Tan, Qixin Wang, Lei Bu, Jiannong Cao, Xue Liu. From Offline toward Real Time: A Hybrid Systems Model Checking and CPS Codesign Approach for Medical Device Plug-and-Play Collaborations, In IEEE Transactions on Parallel and Distributed Systems 25 (3), 642-652, 2014.

Lei Bu, Dingbao Xie. Formal Verification of Hybrid System, Journal of Software (in Chinese), 25(2), 219-233,2014.

Lei Bu, Xuandong Li. Path-Oriented Bounded Reachability Analysis of Composed Linear Hybrid Systems, In International Journal on Software Tools for Technology Transfer, Volume 13, Number 4, pp.307-317, Springer.

Fengling Zhang, Lei Bu, Linzhang Wang, Jianhua Zhao, Xuandong Li. Modeling and Analysis of Wireless Sensor Network Protocols By Stochastic Timed Automata and Statistical Model Checking. In Scientia Sinica Informationis (SCIENCE CHINA Information Sciences, in Chinese), 43(1): 90-107, 2013

Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, and Stefano Tonetta. Model Checking of Hybrid Systems using Shallow Synchronization, In Proceedings of the 30th IFIP International Conference on Formal Methods for Networked and Distributed Systems (FORTE 2010), Amsterdam, Netherlands, 2010, Lecture Notes in Computer Science, Springer, pp.155-169

Lei Bu, Qixin Wang, Xin Chen, Linzhang Wang, Tian Zhang, Jianhua Zhao and Xuandong Li. Toward Online Hybrid Systems Model Checking of Cyber-Physical Systems Time-Bounded Short-Run Behavior, In Proceedings of Proceedings of ACM/IEEE Second International Conference on Cyber-Physical Systems (ICCPS2011), Work-in-Progress Session. In ACM SIGBED Review, Volume 8, Number 2

Lei Bu, You Li, Linzhang Wang, Xin Chen and Xuandong Li. BACH 2: Bounded ReachAbility CHecker for Compositional Linear Hybrid Systems, In Proceedings of the 13th Design Automation & Test in Europe Conference (DATE 2010), Dresden, Germany, pp. 1512-1517, 2010.

Lei Bu, You Li, Linzhang Wang and Xuandong Li. BACH: A Toolset for Bounded Reachability Analysis of Linear Hybrid Systems, Journal of Software (in Chinese), 22(4), 640-658,2011.

Lei Bu, Jianhua Zhao and Xuandong Li. Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming, In Proceeding of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI2010), Madrid, Spain, Lecture Notes in Computer Science 5944, Springer, pp.79-94, 2010.

Minxue Pan, Lei Bu, and Xuandong Li. TASS: Timing Analyzer of Scenario-Based Specifications. In Proceedings of the 21th International Conference on Computer Aided Verification (CAV2009), France, 2009, Lecture Notes in Computer Science 5643, Springer, pp.689-695.

Lei Bu, You Li, Linzhang Wang and Xuandong Li. BACH : Bounded ReachAbility CHecker for Linear Hybrid Automata. In Proceedings of the 8th International Conference on Formal Methods in Computer Aided Design(FMCAD2008). Portland, OR, USA, IEEE Computer Society Press, 2008, pp.65-68.

奖励荣誉

11/2019, NASAC Young Software Innovation Award, Software Engineering Technical Committee and System Software Technical Committee, China Computer Federation

01/2016, Young Talent Development Program, China Computer Federation

09/2014, StarTrack Program Visiting Young Faculty, Microsoft Research Asia

09/2007, Full Scholarship under the State Scholarship Fund by the China Scholarship Council (CSC).

任职情况

12/2018-Present, 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.

学术经历

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.