Lei Bu

Assistant Professor, PH.D.

bulei at nju.edu.cn

Dept. of Computer Science & Technology

Nanjing University,

MMW-508, 22 Hankou Rd., Nanjing, Jiangsu 210093, China

 

 

 

 

 

 

 

 

 

[SEG Group]

[Biography]

[Education]

[Publication]

[Tools]

[Talks ]

[Hobbies]

 

 

 

 

 

 

 

 

 

Biography:

  I am an Assistant Professor in the SEG Group led by Prof. Xuandong Li in Nanjing University. 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]

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.

 

 

 
  • 06/2009, Visiting Scholar in Embedded System Unit, Fondazione Bruno Kessler, Povo, Trento, Italy. Working with Dr. Alessandro Cimatti.

 

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

 

 

 
  • 02/2006-09/2006, Visiting Scholar 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]

Publications:

 

  • Lei Bu, Xuandong Li. Path-Oriented Bounded Reachability Analysis of Composed Linear Hybrid Systems, In International Journal on Software Tools for Technology Transfer, Springer, DOI:10.1007/s10009-010-0163-9.

 

 

 

  • 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

 

 

 

  • You Li, Lu Yang, Lei Bu, Linzhang Wang, Jianhua Zhao, and Xuandong Li. Extending Ada to Support Multi-core Based Monitoring and Fault Tolerance, In Proceedings of the ACM’s Annual International Conference on Ada and Related Technologies Engineering Safe, Secure, and Reliable Software (SIGADA 2010), Fairfax, Virginia, USA, 2010.

 

 

 

  • Xuandong Li, Minxue Pan, Lei Bu, Linzhang Wang, and Jianhua Zhao. Timing Analysis of Scenario-Based Specifications. In Software Testing, Verification and Reliability, Wiley InterScience, DOI:10.1002/stvr.434.

 

 

 

  • 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 Systmes, accepted by Journal of Software (in Chinese), 2009.

 

 

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

 

 

 
  • Bin Lei, Linzhang Wang, Lei Bu, and Xuandong Li. Robustness Testing for Components Based on State Machine Model. In Journal of Software (in Chinese), Vol.21, No.5, 2010, pp.930-941.

 

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

 

 
  • Xuandong Li, Sumit Kumar Jha and Lei Bu. Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming. In Proceedings of the 4th International Workshop on Bounded Model Checking (BMC2006), USA, 2006, ENTCS 174:3, Elsevier Science, pp.57-70, 2007.

 

 
  • Xuandong Li, Lei Bu, Jun Hu, Jianhua Zhao, Tao Zheng and Guoliang Zheng. Scenario-Based Timing Consistency Checking for Time Petri Nets. In Proceedings of the 26th International Conference on Formal Methods for Networked and Distributed Systems (FORTE2006), France, 2006, Lecture Notes in Computer Science 4229, Springer, pp.388-403.

 

 
  • Xuandong Li, Jun Hu, Lei Bu, Jianhua Zhao and Guoliang Zheng. Consistency Checking of Concurrent Models for Scenario-Based Specifications. In Proceedings of the 12th International SDL Forum (SDL2005), Norway, 2005, Lecture Notes in Computer Science 3530, Springer, pp.298-312.

 

 
  • 1 more paper under submission

[Top]

Tools:

[Top]

Talks:  

Non-SEG Talks:

  • 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

  • Dependable System and Productline Demo for Trustie Project, Beijing, January, 2009

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

  • Graphically Presentation of The Behavior of Concurrent System, The University of Texas at Dallas, Dallas, USA, March, 2006

SEG Talks:

  • Key Components and Technology of National High Speed Railway, September, 2009, SEG

  • SMT Methodology, May, 2009, SEG

  • Liveness and Fair termination of LHA, March, 2009, SEG

 

  • Formal Method and System Biology, February, 2009, SEG

 

  • Compositional Reachability of LHA Network, October, 2008, SEG

 

  • Convex Hybrid Automata, September, 2008, SEG

 

  • Aspect Oriented Programming I, II, November, 2005, SEG

 

  • Spin: The Model Checker, March, 2005, SEG

 

  • ...

[Top]

Hobbies:  

  • Reading and Writing

  • Football

  • Movie

  • Music

  • Travelling

  • Photography

[Top]

 

 

Last Updated September 23, 2010