Contact

• Office: No. 616, Room 339, Building 5
• Address: South Fourth Street 4#, Zhong Guan Cun, Beijing
• email: liyong###ios**ac*cn or liyong460###gmail**com

About me

I am currently a Ph.D. student in the group. My main research interests are:

• Probabilistic Model checking
• Linear Temporal Logic and Büchi automata
• Algorithmic Learning
• Termination Analysis

If you are also interested in those topics, please be free to contact me.

Tools

• Regular Omega Language Learning (ROLL)
• Complementing Büchi automata by Learning (Buechic)
• Complementation of Büchi Automata (Buchi) 

Education

• 9/2015 – present: Ph.D. Student in Computer Software and Theory at Institute of Software, Chinese Academy of Sciences and University of Chinese Academy of Sciences
• 9/2013 – 6/2015: Master Student in Computer Software and Theory at Institute of Software, Chinese Academy of Sciences and University of Chinese Academy of Sciences
• 9/2009 – 6/2013: Computer Science and Technology (Bachelor’s degree) at Nanjing University of Posts and Telecommunications

Research stays

• Jul. 11, 2018  – Jul. 26, 2018: Institute of Information Science,  Academia Sinica
• Jan. 27, 2018  – Feb. 9, 2018: Institute of Information Science,  Academia Sinica
• Nov. 3, 2017  – Nov. 18, 2017: Institute of Information Science,  Academia Sinica
• Aug. 22, 2017  – Sept. 6, 2017: Institute of Information Science,  Academia Sinica
• May 17, 2017  – May 31, 2017: Institute of Information Science, Academia Sinica
• Feb. 1, 2016  – Feb. 15, 2016: Dependable Systems and Software Group, Universität des Saarlandes
• Oct. 17, 2015 – Jan. 31, 2016: Software Modelling and Verification Group, RWTH Aachen

Activities

• May 26 – May 27, 2018: 2018 Workshop on SoftWare Analysis and Verification (SAVE 2018), Hangzhou, China (Talked about automata-based termination checking)
• Apr. 7 – Apr.12, 2018: 4th School on Engineering Trustworthy Software Systems (SETSS 2018), Chongqing, China
• Oct. 20 – Oct. 26, 2017: 3rd Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA 2017), Changsha, China
• Apr. 24 – Apr. 28, 2017: 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems  (TACAS 2017), Uppsala, Sweden (Talked about learning Büchi automata)
• Dec. 28 – Dec. 29, 2016: Colloquium on Logic in Engineering Dependable Software (LEDS 2016), Shanghai, China (Talked about learning Büchi automata)
• Nov. 9 – Nov. 11, 2016: 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2016), Beijing, China (Talked about Parametric MC synthesis against PLTL )
• Oct. 17 – Oct. 19, 2016: 23rd International Symposium on Temporal Representation and Reasoning (TIME 2016), Copenhagen, Denmark (Talked about model checking fairness)
• Dec. 6 – Dec. 9, 2015: Dagstuhl seminar on Formal Evaluation of Critical Infrastructures, Dagstuhl, Germany (Talked about model checking fairness)
• Oct. 12 – Oct. 15, 2015: 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), Shanghai, China
• Nov. 23 – Nov. 29, 2014: The Sino-German Workshop on Computation and Reasoning with Constraints, Beijing, China

Conferences

• Advanced Automata-based Algorithms for Program Termination Checking, Chen, Y.-F.; Heizmann, M.; Lengál, O.; Li, Y.; Tsai, M.-H.; Turrini, A. and Zhang, L. In PLDI, pages 135-150, 2018.
• Ultimate Automizer and the Search for Perfect Interpolants (Competition Contribution), Heizmann, M.; Chen, Y.-F.; Dietsch, D.; Greitschus, M.; Hoenicke, J.; Li, Y.; Nutz, A.; Musa, B.; Schilling, C.; Schindler, T. and Podelski, A. In TACAS, LNCS , 2018.
• Learning to Complement Büchi Automata, Li, Y.; Turrini, A.; Zhang, L. and Schewe, S. In VMCAI, pages 313-335, LNCS 10747, 2018.
• A Novel Learning Algorithm for Büchi Automata based on Family of DFAs and Classification Trees, Li, Y.; Chen, Y.-F.; Zhang, L. and Liu, D. In TACAS, pages 208-226, LNCS 10205, 2017.
• Verify LTL with Fairness Assumptions Efficiently, Li, Y.; Song, L.; Feng, Y. and Zhang, L. In TIME, 2016.
• An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties, Li, Y.; Liu, W.; Turrini, A.; Hahn, E. M. and Zhang, L. In SETTA, pages 280-296, LNCS 9984, 2016.
• A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking, van Dijk, T.; Hahn, E. M.; Jansen, D. N.; Li, Y.; Neele, T.; Stoelinga, M.; Turrini, A. and Zhang, L. In Dependable Software Engineering, Theories, Tools, and Applications. First International Symposium (SETTA 2015), pages 35-54, Springer, Lecture Notes in Computer Science 9409, 2015.