•                 Ph.D. Candidate, Sept. 2010 - June 2015 (expected)
•                 463 Winston Chung Hall (formerly Engineering Building Unit 2)
•                 Department of Computer Science and Engineering
•                 University of California, Riverside
•                 900 University Avenue
•                 Riverside, CA 92507
•                 E-mail: ltan003@cs.ucr.edu



•                 Curriculum Vitae

Brief Biography

Currently, I am a second year Ph.D. candidate in Computer Science at UC Riverside, working with Dr. Rajiv Gupta. 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 and professional homepage at .

My primary research interests are in the following areas:

• Parallel Programming
• Software Debugging and Program Analysis
• Software Verification

News

• 01/25/2012: I advanced to PhD candidacy, finally.
• 11/22/2011: I tried to schedule the PhD Qualifying Exam before 2012 but failed due to my bad talk given on 11/09/2011 as a rehearsal. - No preparation, no success; No taking suggestions from others, no success.
• 07/17/2011: First summer, busy summer.
• 06/17/2011: I succeeded in finishing all my courses in one year before further Ph.D. research.
• 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 - 06/2015 (expected)
  Advisor: Dr. Rajiv Gupta

• 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. "A Well-typed Lightweight Situation Calculus", in Proceedings of the 21st Workshop on Logic-based methods in Programming Environments (WLPE'11), 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'11)},
  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'11), 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'11)},
  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'10), 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'10)},
  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'09), 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'09)},
  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

• Debugging Parallelized Programs

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

Teaching Experience

• CS   6: "Effective Use of the World Wide Web" by Dr. Brian Linard, Fall 2011 (in charge of Web Design 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" by Dr. Brian Linard, Fall 2011, Winter 2012, Spring 2012 (in charge of Assembly Programming) [Office Hours]
  • Spring 2012: 10am-12pm on Fridays for Section 21 & 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 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 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 finger.