Lei Bu

Associate Professor, PH.D.

Dept. of Computer Science & Technology

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]

[Tools]

[Talks ]

[Fundings]


News:

 

 

 

 

[Top]


Short Biography:

 

I am an Associate Professor in the Software Engineering Group led by Prof. Xuandong Li in Dept. of Computer Science and Technology, 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:

 

  • 12/2013-Present, 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:

 

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

[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 ( 18 Autumn, 17 Autumn, 16 Autumn, 15 Autumn, Open to both undergraduate and graduate students)

 

 

 

  • Practice of Fundamental Programming (18 Spring, 17 Spring, 16 Spring, 15 Spring, Open to undergraduate students)

 

 

 

  • Formal Language and Automata ( 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]


Selected Publications:

Full list please refer My Google Scholar Profile ; My DBLP

 

  • 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, To Appear.

 

 

 

  • 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

 

 

 

  • Yang Yang, Lei Bu, Xuandong Li. Forward and Backward: Bounded Model Checking of Linear Hybrid Automata From Two Directions. In Proceedings of the 12th International Conference on Formal Methods in Computer Aided Design (FMCAD2012), USA, IEEE Computer Society Press, 2012

 

 

 

  • Lei Bu, Dingbao Xie, Xin Chen, Linzhang Wang, and Xuandong Li. Demo Abstract: BACHOL - Modeling and Verification of Cyber-Physical Systems Online. In Proceedings of The ACM/IEEE Third International Conference on Cyber-Physical Systems (ICCPS2012), pp.222, IEEE Computer Sciety, 2012.

 

 

 

  • Lei Bu, Yang Yang, Xuandong Li. IIS-Guided DFS for Efficient Bounded Reachability Analysis of Linear Hybrid Automata. In Proceedings of Haifa Verification Conference (HVC 2011), Israel, Lecture Notes in Computer Science 7261, Springer, 2012, pp.35-49.

 

 

 

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

 

 

[Top]


Tools:

 

 

 

 

[Top]


Talks:  

 

 

Tutorial:

  • 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
   

Invited Talks:

  • Model Checking and Application of Real time Hybrid System. Young Scientist Forum, NASAC 2015, Wuhan, November, 2015
   

  • Hybrid Automata: On Bounded Reachability Checking Guided by Analysis of Infeasible Path Segments, and on Derivation of Global Properties. ISCAS, Beijing, January, 2015
   

  • Deriving Unbounded Proof of Linear Hybrid Automata From Bounded Verification. Sino-German CDZ Workshop, Beijing, November, 2014
   

  • Online Modeling and Verification of Cyber-Physical System. SUTD, Singapore, May, 2014
   

  • SAT-LP-IIS Joint-directed Path-Oriented Bounded Reachability Analysis of Linear Hybrid Automata. NII, Tokyo, Japan, January, 2014
   

  • SAT-LP-IIS Joint-directed Path-Oriented Bounded Reachability Analysis of Linear Hybrid Automata. Sino-German Symposium on Verification of Hybrid System, Beijing, September, 2013
   

  • Path-oriented Bounded Model Checking of Linear Hybrid Automata. Jiangsu Computer Federation Software Special Interest Committee 2013 Annual Meeting, Wuxi, December, 2012
   

  • Bidirectional DFS Based BMC of LHA. Sino-German Symposium on Formal Application of Train-Control System, Institute of Software, Beijing, September, 2012.
   

  • BACH: Bounded Model Checker for LHA . Sino-German Symposium on Distributed Simulation and Computational System Biology. NUDT, Changsha, February, 2011.
   

Other Selected Talks:

  • Deriving Unbounded Proof of Linear Hybrid Automata From Bounded Verification, RTSS 2014, Nanjing, Rome, Italy, December, 2014
   

  • Online Hybrid Automata Verification of Dynamical Cyber-Physical System, Clarke Symposium 2014, Carnegie Mellon University, Pittsburgh, PA, U.S.A., September, 2014
   

  • Bidirectional DFS Based BMC of LHA. FMCAD 2012, Cambridge, UK, October, 2012
   

  • Modeling and Analysis of Wireless Sensor Network Protocols By Stochastic Timed Automata and Statistical Model Checking, Scientia Sinica Informationis Special Symposium, Nanjing, China, October, 2012
   

  • From Offline toward Real-Time: A Hybrid Systems Model Checking and CPS Co-Design Approach for Medical Device Plug-and-Play (MDPnP), ICCPS 2012, Beijing, China, April, 2012
   

  • IIS-Guided DFS Based BMC of LHA. HVC 2011, Haifa, Israel, December, 2011
   

  • Toward Online Hybrid Systems Model Checking of Cyber-Physical Systems Time-Bounded Short-Run Behavior, ICCPS 2011, Chicago, US, April, 2011
   

  • BACH2: Bounded Reachability Checker for Compositional Linear Hybrid Systems, DATE 2010, Dresden, Germany, March, 2010
   

  • Path-oriented Reachability Verification of Convex Hybrid Automata, VMCAI 2010, Madrid, Spain, January, 2010
   

  • Bounded Reachability of Compositional LHA Network using BACH2.0, Fondazione Bruno Kessler, Trento, Italy, June, 2009
   

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

[Top]


Fundings:  

 

 

Ongoing Projects:

 

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

 

 

Completed Projects:

 

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

[Top]

   
 

 

Last Updated March, 2018