Brief Biography

Currently, I am a third year Ph.D. candidate in Computer Science at UC Riverside, working with Dr. Zizhong Chen. Prior to coming to UCR CSE, I received both my B.S. and M.S. degrees in Computer Science with distinction from East China Normal University, Shanghai, China in 2008 and 2010, respectively. You may refer to my old homepage at ECNU, academic homepage at Google Scholar Citations, and professional homepage at .

My primary research interests are in the following areas: Energy Efficient High Performance Computing via Software Managing the Hardware Fault Detection via Software Debugging and Program Analysis Software Verification via Formal Methods

News

• 10/29/2012: One paper has been accepted by CGO'13 with the acceptance rate of 28.2%.
• 01/25/2012: I advanced to PhD candidacy, finally.
• 05/26/2010: I have already graduated from ECNU and I really enjoyed the 6 years of being an ECNUer and the life in Shanghai. Thanks, all friends! See you in 5 years, hopefully.

Education

• University of California, Riverside (UCR), Riverside, CA, USA
  Ph.D. Candidate in Computer Science, 09/2010 - present
  Advisor: Dr. Zizhong Chen

• East China Normal University (ECNU), Shanghai, China
  M.S. in Computer Science, 09/2008 - 06/2010
  Thesis: "A Research of UML Formal Verification Based on Situation Calculus and OCL Constraints Automatic Generation". [Abstract] [Talk] [Prototype Tool Snapshot]
  Advisor: Prof. Zongyuan Yang

• East China Normal University (ECNU), Shanghai, China
  B.S. in Computer Science, 09/2004 - 06/2008
  Thesis: "AJAX based Real-Time Teaching Website for the Course 'Principles of Compiler'". [Abstract] [Talk] [Website]
  Thesis Advisor: Prof. Zongyuan Yang

Publications

• Journal Articles:
  
  See My Master's Contributions
  
  
  Li Tan, Zongyuan Yang, and Jinkui Xie. "Data Response Optimization of the AJAX Technology" (in Chinese), in Journal of Computer Engineering, Vol. 36, No. 7, pp. 52-54, Apr. 2010.
  [Abstract] [Talk] [DOI]
  
  To summarize an optimized model of AJAX which is more efficient and secure, this paper analyzes the working principle and data transmission performance of AJAX and discusses the difference between XML and JSON by experiments with a focus on the format of response data returned. Furthermore, some suggestions for choosing either based on the current application scenarios are given, which improves the shortcomings such as data response redundancy caused by AJAX nowadays.


• Conference and Workshop Papers:
  
  
  • Li Tan, Min Feng, and Rajiv Gupta. "Lightweight Fault Detection in Parallelized Programs", in Proceedings of the 11th ACM/IEEE International Symposium on Code Generation and Optimization (CGO), pp. 12-22, Shenzhen, China, Feb. 2013. Acceptance Rate: 28.2% (33/117)
  [Abstract] [Talk] [DOI] [BibTeX]
  
  A popular approach for producing parallel software is to develop a sequential version of an application and then incrementally introduce parallel constructs to parallelize different parts of the application. During the parallelization process, programming errors may be introduced, causing concurrency bugs. In this paper we develop a technique for runtime detection of data dependence faults (i.e., data races and atomicity violations) introduced during parallelization. By leveraging the availability of two versions of the program, the sequential one the the parallelized one, we comparison check dynamic data dependences exercised during executions of the two versions to identify faults.
  To reduce the cost of comparison checking we develop three optimizations. The first optimization causes only a subset of dynamically exercised data dependences to be comparison checked. The second optimization shows that not all instances of a dynamically exercised data dependence need to be comparison checked. The third optimization shows that static analysis of parallelizing constructs can be exploited to eliminate the need for executing the parallelized version altogether. In addition, our solution is applicable when different program executions on the same input may follow different execution paths, it is effective in situations where the fault introduced manifests itself rarely during execution, and it is also effective in pinpointing the location of the fault in the program. We implemented and evaluated our approach using ten benchmarks. The experimental results indicate an average slowdown of 3x to perform fault detection.
  
  @inproceedings{CGO13,
  author = {Li Tan and Min Feng and Rajiv Gupta},
  title = {Lightweight Fault Detection in Parallelized Programs},
  booktitle = {Proceedings of the 11th ACM/IEEE International Symposium on Code Generation and Optimization (CGO)},
  year = {2013},
  pages = {12--22},
  location = {Shenzhen, China},
  publisher = {IEEE},
  doi = {http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=06494979},
  }
  
  
  • Li Tan. "A Well-typed Lightweight Situation Calculus", in Proceedings of the 21st Workshop on Logic-based methods in Programming Environments (WLPE), ICLP 2011 Workshop, pp. 62-73, Lexington, Kentucky, USA, July 2011.
  [Abstract] [Talk] [DOI] [BibTeX]
  
  Situation calculus has been widely applied in Artificial Intelligence related fields. This formalism is considered as a dialect of logic programming language and mostly used in dynamic domain modeling. However, type systems are hardly deployed in situation calculus in the literature. To achieve a correct and sound typed program written in situation calculus, adding typing elements into the current situation calculus will be quite helpful. In this paper, we propose to add more typing mechanisms to the current version of situation calculus, especially for three basic elements in situation calculus: situations, actions and objects, and then perform rigid type checking for existing situation calculus programs to find out the well-typed and ill-typed ones. In this way, type correctness and soundness in situation calculus programs can be guaranteed by type checking based on our type system. This modified version of a lightweight situation calculus is proved to be a robust and well-typed system.
  
  @inproceedings{WLPE11,
  author = {Li Tan},
  title = {A Well-typed Lightweight Situation Calculus},
  booktitle = {Proceedings of the 21st Workshop on Logic-based methods in Programming Environments (WLPE)},
  year = {2011},
  pages = {62--73},
  location = {Lexington, Kentucky, USA},
  editor = {Peter Schneider-Kamp},
  doi = {http://arxiv.org/abs/1201.2430},
  }
  
  See My Master's Contributions
  
  
  Li Tan, Zongyuan Yang, and Jinkui Xie. "Verifying UML in Prolog", in Proceedings of the 10th IASTED International Conference on Software Engineering (SE), pp. 1-8, Innsbruck, Austria, Feb. 2011.
  [Abstract] [DOI] [BibTeX]
  
  From the viewpoint of software life cycle in Software Engineering, software architecture is the core of the structure and behavior of software. As software architecture design itself is a kind of modeling activity, how to verify the correctness of the standard modeling language of software architecture design, UML, is one big problem. This paper uses an implementation of situation calculus, Prolog, as an underlying logic framework to formally describe a subset of UML diagrams, a graphic notation, and assigns it an equivalent formal semantics automatically via our prototype tool, USCVSC. Then we verify possible syntax and semantic errors in UML in a Prolog interpreter, SWI-Prolog, after a definition of error types in UML. Finally, a goal is achieved that software designers could correct the design of UML diagrams prior to fixing bugs in code in the phase of test, which avoids unnecessary system overhead in the following phases of Software Engineering with the hope of enhancing the overall efficiency of the process of Software Engineering.
  
  @inproceedings{SE11,
  author = {Li Tan and Zongyuan Yang and Jinkui Xie},
  title = {Verifying UML in Prolog},
  booktitle = {Proceedings of the 10th IASTED International Conference on Software Engineering (SE)},
  year = {2011},
  pages = {1--8},
  location = {Innsbruck, Austria},
  publisher = {ACTA Press},
  doi = {http://dx.doi.org/10.2316/P.2011.720-036},
  }
  
  
  Li Tan, Zongyuan Yang, and Jinkui Xie. "OCL Constraints Automatic Generation for UML Class Diagram", in Proceedings of the International Conference on Software Engineering and Service Science (ICSESS), pp. 392-395, Beijing, China, July 2010.
  [Abstract] [DOI] [BibTeX]
  
  As a standard modeling language of software architecture design, UML lacks formal semantics on account of its informal graphical notation. To further provide refined description of UML, OCL is primarily and widely employed. Generally, OCL constraints are written manually, which may cause incorrectness and extra overhead. Therefore, generating OCL constraints template for UML models is a superior solution. The OCL constraints template automatically generated can be used as a reference for software designers. First of all, the significance of automatic generation of OCL constraints was emphasized, and then the application domain of OCL was shown, followed by a lexical analysis of how to extract the target objects in UML models where OCL constraints were needed to build and an algorithm of extraction. Eventually, this extraction algorithm was implemented by Perl. In our way, the overall quality and efficiency of software design is enhanced and thus contributions are made for the automation of Software Engineering.
  
  @inproceedings{ICSESS11,
  author = {Li Tan and Zongyuan Yang and Jinkui Xie},
  title = {OCL Constraints Automatic Generation for UML Class Diagram},
  booktitle = {Proceedings of the International Conference on Software Engineering and Service Science (ICSESS)},
  year = {2010},
  pages = {392--395},
  location = {Beijing, China},
  publisher = {IEEE},
  doi = {http://dx.doi.org/10.1109/ICSESS.2010.5552361},
  }
  
  
  Li Tan, Zongyuan Yang, and Jinkui Xie. "UCVSC: A Formal Approach to UML Class Diagram Online Verification Based on Situation Calculus", in Proceedings of the 4th International Conference on Computer Sciences and Convergence Information Technology (ICCIT), pp. 375-380, Seoul, Korea, Nov. 2009.
  [Abstract] [Talk] [DOI] [BibTeX]
  
  The gap between informal models used in a UML environment and formal verifications and proofs in academic research prevents UML from valid and efficient application. In this paper, we propose an approach to bridge the gap between UML class diagram and situation calculus via our formal verification tool, UCVSC (UML Class diagram online Verification based on Situation Calculus). UML class diagram describes a software system informally while situation calculus is employed as the underlying formalism to precisely specify the system. With respect to most components in UML class diagram, the strength of reasoning about actions and describing the state of the world in situation calculus can be applied to represent them appropriately. Using UML tools and predefined mapping mechanism, we transformed UML class diagram to XMI, an intermediate format, and finally to situation calculus in Prolog syntax. This approach attempts to provide precise semantics of UML class diagram which can be logically verified. In addition, we automated the verification process in an online prototype system. Furthermore, a case study on an academic system is presented to illustrate and evaluate our approach.
  
  @inproceedings{ICCIT09,
  author = {Li Tan and Zongyuan Yang and Jinkui Xie},
  title = {UCVSC: A Formal Approach to UML Class Diagram Online Verification Based on Situation Calculus},
  booktitle = {Proceedings of the 4th International Conference on Computer Sciences and Convergence Information Technology (ICCIT)},
  year = {2009},
  pages = {375--380},
  location = {Seoul, Korea},
  publisher = {IEEE & ACM},
  doi = {http://dx.doi.org/10.1109/ICCIT.2009.307},
  }


• Miscellaneous Papers:
  
  See My Master's Contributions
  
  
  Lei A, Jinxia Xie, and Li Tan. "Using Multiple Regression Analysis in the Prediction of Urban Employment in China" (in Chinese), finished in Sept. 2009.
  [Abstract]
  
  This paper compares incremental sum of squares of regression of influential factors of urban employment in China with each other by according data analysis and statistics tools, and then concludes the degree of influence of these factors. Based on multiple regression analysis and Trend Extrapolation, linear multiple regression model is founded and checked. Furthermore, this model is refined by industries, regions and employment establishments. Considering relevant national policies and plans, prediction of urban employment in China in 2009 and 2010 is made. Finally, according to the importance of influential factors and current social condition, possible extension of the model and suggestions of solving urban employment problem are given.

Research Experience

• Energy Efficiency of Numerical Linear Algebra Algorithms and Software in High Performance Computing

• Debugging Parallelized Programs [CGO'13]

• Situation Calculus Based UML Class and State Diagram Online Verification System [ICCIT'09] [ICSESS'10] [SE'11]
• AJAX Data Response Optimization [JCE'10]

Released Tools

• USCVSC: An online tool for UML State & Class diagram Verification based on Situation Calculus

Industrial Experience

• PHP Web Developer, Resumebook.tv, LLC, CA, USA, Oct. - Dec. 2010
• IT Consultant, Gaotime Co., Ltd., Shanghai, China, May - July 2010
• ASP & PHP Web Developer, University Website Editorial Office, ECNU, Feb. 2009 - June. 2010. [Work Snapshot]
• Intel C/C++ Compiler Document Translator, SinoBot Inc., Shanghai, China, July - Aug. 2008
• Windows System Management Engineer, Xinmin Evening Paper, Shanghai, China, July - July 2008
• UNIX System Management Engineer, eBay Inc. China Operation Center, Shanghai, China, July 2007 - Jan. 2008. [Work Snapshot]
• ASP Web Developer, Firstlat Info. & Tech. Co., Ltd., Shanghai, China, July - July 2007

Professional Services

• CASES (2011), RV (2011), APLAS (2011), IPDPS-PDSEC (2013)

Teaching Experience

• CS     6: "Effective Use of the World Wide Web" instructed by Dr. Brian Linard, Fall 2011 (in charge of website designing and building in HTML) [Office Hours]
  • Fall 2011: 2pm-3pm on Fridays for Section 21 & 25 at 463 WCH
• CS   61: "Machine Organization and Assembly Language Programming" instructed by Dr. Brian Linard, Fall 2011, Winter 2012, and Spring 2012 (in charge of assembly programming) [Office Hours]
  • Summer 2012: 1pm-2pm on Mondays & 1pm-2pm on Wednesdays for Section 121 at 463 WCH
  • Spring 2012: 9pm-10pm on Wednesdays for Section 21 & 1pm-2pm on Fridays for Section 22 at 463 WCH
  • Winter 2012: 9am-11am on Fridays for Section 21 & 22 at 463 WCH
  • Fall 2011: 10am-11am on Fridays for Section 21 at 463 WCH
• CS 206: "Testing and Verification Techniques in Software Engineering" instructed by Dr. Rajiv Gupta, Fall 2012 [Office Hours]
  • Fall 2012: At 463 WCH, time by appointment
• CS 160: "Concurrent Programming and Parallel Systems" instructed by Dr. Zizhong Chen, Winter 2013 [Office Hours]
  • Winter 2013: 5pm-6pm on Fridays for Section 21 at 465 WCH
• CS 161: "Design and Architecture of Computer Systems" instructed by Dr. Laxmi N. Bhuyan and Dr. Zizhong Chen, Spring 2013 [Office Hours]
  • Spring 2013: 2:00pm-4:00pm on Mondays for Section 22 at 465 WCH

• CS junior course: "Principles of Compilers", Feb. - July 2009
• CS senior course: "Practice in Principles of Compilers", Sept. 2008 - Jan. 2009

My Anecdotes

• My birthday is the Chinese New Year's Day (Chinese Spring Festival based on the Lunar Calendar System). Thanks to my mother, and of course my father.
• My marathon record by far is 03:54:05.
• I start to play basketball since 11. I'm able to spin a ball on any one finger.