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 Associate Research Professor in the group. My main research interests are, but not limited to, the following:

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

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

You can also visit my homepage on GitHub for more information about my research works.

Tools

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

Education

• 10/2022 – present: Associate Research Professor at Institute of Software, Chinese Academy of Sciences
• 2/2020 – 10/2022: Research Assistant at Institute of Software, Chinese Academy of Sciences
• 9/2015 – 1/2020: 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

• Feb. 1, 2019 – Jun. 30, 2019: Department of Computer Science, Rice University
• 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

• Synthesizing Good-Enough Strategies for LTLf Specifications. Li, Y., Turrini, A., Vardi, M. Y., & Zhang, L.
• Congruence Relations for  B\” uchi Automata. Li, Y., Tsay, Y. K., Turrini, A., Vardi, M. Y., & Zhang, L. (2021).  arXiv preprint arXiv:2104.03555.
• Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications, Bansal, S.; Li, Y.; Tabajara, L. M. and Vardi, M. Y. In AAAI, pages 9766-9774, 2020.
• Modelling and Implementation of Unmanned Aircraft Collision Avoidance, Feng, W.; Huang, C.-C.; Turrini, A. and Li, Y. In SETTA, pages 52-69, Springer, Lecture Notes in Computer Science 12153, 2020.
• SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM, Li, X.; Li, Y.; Li, Y.; Sun, X.; Turrini, A. and Zhang, L. In ESEC/FSE, pages 1635-1639, ACM, 2020.
• Proving Non-Inclusion of Büchi Automata based on Monte Carlo Sampling, Li, Y.; Turrini, A.; Sun, X. and Zhang, L. In ATVA, pages 467-483, Springer, LNCS 12302, 2020.
• On the Power of Unambiguity in Büchi Complementation, Li, Y.; Vardi, M. Y. and Zhang, L. In GANDALF, pages 182-198, Electronic Proceedings in Theoretical Computer Science 326, 2020.
• Synthesizing Nested Ranking Functions for Loop Programs via SVM, Li, Y.; Sun, X.; Li, Y.; Turrini, A. and Zhang, L. In ICFEM, pages 438-454, LNCS 11852, 2019.
• ROLL 1.0: ω-Regular Language Learning Library, Li, Y.; Sun, X.; Turrini, A.; Chen, Y.-F. and Xu, J. In TACAS, pages 365-371, LNCS 11427, 2019.
• 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, pages 447-451, Springer, LNCS 10806, 2018.
• Learning to Complement Büchi Automata, Li, Y.; Turrini, A.; Zhang, L. and Schewe, S. In VMCAI, pages 313-335, Springer, 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, pages 41-50, IEEE Computer Society, 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.

Professional Activities

• TACAS 2019 Artifact Evaluation PC member