Contact
- Office: Room A218, Building 5
- Address: South Fourth Street 4#, Zhong Guan Cun, Beijing
- email:
liyong###ios**ac*cnorliyong460###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
- Oct. 2022 – present: Associate Research Professor at Institute of Software, Chinese Academy of Sciences
- Feb. 2020 – Oct. 2022: Research Assistant at Institute of Software, Chinese Academy of Sciences
- Sept. 2015 – Jan. 2020: Ph.D. Student in Computer Software and Theory at Institute of Software, Chinese Academy of Sciences and University of Chinese Academy of Sciences
- Sept. 2013 – Jun. 2015: Master Student in Computer Software and Theory at Institute of Software, Chinese Academy of Sciences and University of Chinese Academy of Sciences
- Sept. 2009 – Jun. 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
Publications
- : DAG-Based Compositional Approaches for LTLf to DFA Conversions. In Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design - FMCAD 2024, pages 227-235, 2024. DOI
- : DFAMiner: Mining Minimal Separating DFAs from Labelled Samples. In Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II, volume 14934 of Lecture Notes in Computer Science, pages 48-66, 2024. DOI BIB
- : Angluin-Style Learning of Deterministic Büchi and Co-Büchi Automata. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, August 03-09, 2024, Jeju, Republic of Korea, 2024.
- : Singly exponential translation of alternating weak Büchi automata to unambiguous Büchi automata. In Theor. Comput. Sci. 1006:114650, 2024. DOI BIB
- : Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata. In 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium, volume 279 of LIPIcs, pages 37:1-37:17, 2023. DOI BIB
- : Model Checking Strategies from Synthesis over Finite Traces. In Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I, volume 14215 of Lecture Notes in Computer Science, pages 227-247, 2023. DOI BIB
- : On the power of finite ambiguity in Büchi complementation. In Inf. Comput. 292:105032, 2023. DOI BIB
- : Quantitative controller synthesis for consumption Markov decision processes. In Inf. Process. Lett. 180:106342, 2023. DOI BIB
- : Modular Mix-and-Match Complementation of Büchi Automata. In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I, volume 13993 of Lecture Notes in Computer Science, pages 249-270, 2023. DOI BIB
- : A Novel Family of Finite Automata for Recognizing and Learning ω-Regular Languages. In Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I, volume 14215 of Lecture Notes in Computer Science, pages 53-73, 2023. DOI BIB
- : Compositional Safety LTL Synthesis. In Verified Software. Theories, Tools and Experiments - 14th International Conference, VSTTE 2022, Trento, Italy, October 17-18, 2022, Revised Selected Papers, volume 13800 of Lecture Notes in Computer Science, pages 1-19, 2022. DOI BIB
- : EPMC Gets Knowledge in Multi-agent Systems. In Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings, volume 13182 of Lecture Notes in Computer Science, pages 93-107, 2022. DOI BIB
- : Synthesizing ranking functions for loop programs via SVM. In Theor. Comput. Sci. 935:1-20, 2022. DOI BIB
- : Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. In Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 152-173, 2022. DOI BIB
- : Towards a Grand Unification of Büchi Complementation Constructions. In Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660 of Lecture Notes in Computer Science, pages 185-207, 2022. DOI BIB
- : CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). In Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Berlin, Germany, September 26-30, 2022, Proceedings, volume 13550 of Lecture Notes in Computer Science, pages 324-331, 2022. DOI BIB
- : A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. In Inf. Comput. 281:104678, 2021. DOI BIB
- : Congruence Relations for Büchi Automata. In Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 465-482, 2021. DOI BIB
- : Synthesizing Good-Enough Strategies for LTLf Specifications. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 4144-4151, 2021. DOI BIB
- : Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of Lecture Notes in Computer Science, pages 467-483, 2020. DOI BIB
- : Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 9766-9774, 2020. DOI BIB
- : Modelling and Implementation of Unmanned Aircraft Collision Avoidance. In Dependable Software Engineering. Theories, Tools, and Applications - 6th International Symposium, SETTA 2020, Guangzhou, China, November 24-27, 2020, Proceedings, volume 12153 of Lecture Notes in Computer Science, pages 52-69, 2020. DOI BIB
- : SVMRanker: a general termination analysis framework of loop programs via SVM. In ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, November 8-13, 2020, pages 1635-1639, 2020. DOI BIB
- : On the Power of Unambiguity in Büchi Complementation. In Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020, volume 326 of EPTCS, pages 182-198, 2020. DOI BIB
- : Synthesizing Nested Ranking Functions for Loop Programs via SVM. In Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, volume 11852 of Lecture Notes in Computer Science, pages 438-454, 2019. DOI BIB
- : ROLL 1.0: ω-Regular Language Learning Library. In Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, volume 11427 of Lecture Notes in Computer Science, pages 365-371, 2019. DOI BIB
- : Advanced automata-based algorithms for program termination checking. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 135-150, 2018. DOI BIB
- : Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II, volume 10806 of Lecture Notes in Computer Science, pages 447-451, 2018. DOI BIB
- : Learning Büchi Automata and Its Applications. In Engineering Trustworthy Software Systems - 4th International School, SETSS 2018, Chongqing, China, April 7-12, 2018, Tutorial Lectures, volume 11430 of Lecture Notes in Computer Science, pages 38-98, 2018. DOI BIB
- : Learning to Complement Büchi Automata. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, volume 10747 of Lecture Notes in Computer Science, pages 313-335, 2018. DOI BIB
- : A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, volume 10205 of Lecture Notes in Computer Science, pages 208-226, 2017. DOI BIB
- : An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties. In Dependable Software Engineering: Theories, Tools, and Applications - Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings, volume 9984 of Lecture Notes in Computer Science, pages 280-296, 2016. DOI BIB
- : Verify LTL with Fairness Assumptions Efficiently. In 23rd International Symposium on Temporal Representation and Reasoning, TIME 2016, Kongens Lyngby, Denmark, October 17-19, 2016, pages 41-50, 2016. DOI BIB
- : A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. In Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings, volume 9409 of Lecture Notes in Computer Science, pages 35-51, 2015. DOI BIB
Professional activities
- TACAS 2019 Artifact Evaluation PC member