2023
Feng, W., Li, Y., Turrini, A., Vardi, M. Y., & Zhang, L. (2023). On the power of finite ambiguity in Büchi complementation. Information and Computation, 292, 105032. doi:10.1016/j.ic.2023.105032DOI: 10.1016/j.ic.2023.105032
A Novel Family of Finite Automata for Recognizing and Learning $$\omega $$-Regular Languages (Chapter)
Li, Y., Schewe, S., & Tang, Q. (2023). A Novel Family of Finite Automata for Recognizing and Learning $$\omega $$-Regular Languages. In Automated Technology for Verification and Analysis (pp. 53-73). Springer Nature Switzerland. doi:10.1007/978-3-031-45329-8_3DOI: 10.1007/978-3-031-45329-8_3
Model Checking Strategies from Synthesis over Finite Traces (Chapter)
Bansal, S., Li, Y., Tabajara, L. M., Vardi, M. Y., & Wells, A. (2023). Model Checking Strategies from Synthesis over Finite Traces. In Automated Technology for Verification and Analysis (pp. 227-247). Springer Nature Switzerland. doi:10.1007/978-3-031-45329-8_11DOI: 10.1007/978-3-031-45329-8_11
Modular Mix-and-Match Complementation of Büchi Automata (Chapter)
Havlena, V., Lengál, O., Li, Y., Šmahlíková, B., & Turrini, A. (2023). Modular Mix-and-Match Complementation of Büchi Automata. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 249-270). Springer Nature Switzerland. doi:10.1007/978-3-031-30823-9_13DOI: 10.1007/978-3-031-30823-9_13
2022
Fu, C., Hahn, E. -M., Li, Y., Schewe, S., Sun, M., Turrini, A., & Zhang, L. (2022). EPMC Gets Knowledge in Multi-Agent Systems. In International Conference on Verification, Model Checking, and Abstract Interpretation.
CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper) (Chapter)
Yu, S., Dong, Y., Liu, J., Li, Y., Wu, Z., Jansen, D. N., & Zhang, L. (2022). CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). In Unknown Book (Vol. 13550, pp. 324-331). doi:10.1007/978-3-031-17108-6_20DOI: 10.1007/978-3-031-17108-6_20
Divide-and-Conquer Determinization of Buchi Automata Based on SCC Decomposition (Chapter)
Li, Y., Turrini, A., Feng, W., Vardi, M. Y., & Zhang, L. (2022). Divide-and-Conquer Determinization of Buchi Automata Based on SCC Decomposition. In Unknown Book (Vol. 13372, pp. 152-173). doi:10.1007/978-3-031-13188-2_8DOI: 10.1007/978-3-031-13188-2_8
Towards a Grand Unification of Büchi Complementation Constructions (Chapter)
Vardi, M. Y., Fogarty, S., Li, Y., & Tsay, Y. -K. (2022). Towards a Grand Unification of Büchi Complementation Constructions. In Lecture Notes in Computer Science (pp. 185-207). Springer Nature Switzerland. doi:10.1007/978-3-031-22337-2_9DOI: 10.1007/978-3-031-22337-2_9
2021
A novel learning algorithm for Buchi automata based on family of DFAs and classification trees (Journal article)
Li, Y., Chen, Y. -F., Zhang, L., & Liu, D. (2021). A novel learning algorithm for Buchi automata based on family of DFAs and classification trees. INFORMATION AND COMPUTATION, 281. doi:10.1016/j.ic.2020.104678DOI: 10.1016/j.ic.2020.104678
Congruence Relations for Buchi Automata (Chapter)
Li, Y., Tsay, Y. -K., Turrini, A., Vardi, M. Y., & Zhang, L. (2021). Congruence Relations for Buchi Automata. In Unknown Book (Vol. 13047, pp. 465-482). doi:10.1007/978-3-030-90870-6_25DOI: 10.1007/978-3-030-90870-6_25
Synthesizing Good-Enough Strategies for LTLf Specifications (Conference Paper)
Li, Y., Turrini, A., Vardi, M. Y., & Zhang, L. (2021). Synthesizing Good-Enough Strategies for LTLf Specifications. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/ijcai.2021/570DOI: 10.24963/ijcai.2021/570
2020
SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM (Conference Paper)
Li, X., Li, Y., Li, Y., Sun, X., Turrini, A., & Zhang, L. (2020). SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM. In PROCEEDINGS OF THE 28TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (ESEC/FSE '20) (pp. 1635-1639). doi:10.1145/3368089.3417930DOI: 10.1145/3368089.3417930
On the Power of Unambiguity in Büchi Complementation (Journal article)
Li, Y., Vardi, M. Y., & Zhang, L. (n.d.). On the Power of Unambiguity in Büchi Complementation. Electronic Proceedings in Theoretical Computer Science, 326, 182-198. doi:10.4204/eptcs.326.12DOI: 10.4204/eptcs.326.12
Modelling and Implementation of Unmanned Aircraft Collision Avoidance (Chapter)
Feng, W., Huang, C. -C., Turrini, A., & Li, Y. (2020). Modelling and Implementation of Unmanned Aircraft Collision Avoidance. In Dependable Software Engineering. Theories, Tools, and Applications (pp. 52-69). Springer International Publishing. doi:10.1007/978-3-030-62822-2_4DOI: 10.1007/978-3-030-62822-2_4
Proving Non-inclusion of Buchi Automata Based on Monte Carlo Sampling (Chapter)
Li, Y., Turrini, A., Sun, X., & Zhang, L. (2020). Proving Non-inclusion of Buchi Automata Based on Monte Carlo Sampling. In Unknown Book (Vol. 12302, pp. 467-483). doi:10.1007/978-3-030-59152-6_26DOI: 10.1007/978-3-030-59152-6_26
2019
Learning Büchi Automata and Its Applications (Chapter)
Li, Y., Turrini, A., Chen, Y. -F., & Zhang, L. (2019). Learning Büchi Automata and Its Applications. In Engineering Trustworthy Software Systems (pp. 38-98). Springer International Publishing. doi:10.1007/978-3-030-17601-3_2DOI: 10.1007/978-3-030-17601-3_2
ROLL 1.0: ω-Regular Language Learning Library (Chapter)
Li, Y., Sun, X., Turrini, A., Chen, Y. -F., & Xu, J. (2019). ROLL 1.0: ω-Regular Language Learning Library. In Unknown Book (Vol. 11427, pp. 365-371). doi:10.1007/978-3-030-17462-0_23DOI: 10.1007/978-3-030-17462-0_23
Synthesizing Nested Ranking Functions for Loop Programs via SVM (Chapter)
Li, Y., Sun, X., Li, Y., Turrini, A., & Zhang, L. (2019). Synthesizing Nested Ranking Functions for Loop Programs via SVM. In Formal Methods and Software Engineering (pp. 438-454). Springer International Publishing. doi:10.1007/978-3-030-32409-4_27DOI: 10.1007/978-3-030-32409-4_27
2018
Advanced Automata-Based Algorithms for Program Termination Checking (Conference Paper)
Chen, Y. -F., Heizmann, M., Lengal, O., Li, Y., Tsai, M. -H., Turrini, A., & Zhang, L. (2018). Advanced Automata-Based Algorithms for Program Termination Checking. In ACM SIGPLAN NOTICES Vol. 53 (pp. 135-150). doi:10.1145/3192366.3192405DOI: 10.1145/3192366.3192405
Li, Y., Turrini, A., Zhang, L., & Schewe, S. (2018). Learning to Complement Buchi Automata. In VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2018) Vol. 10747 (pp. 313-335). doi:10.1007/978-3-319-73721-8_15DOI: 10.1007/978-3-319-73721-8_15
Ultimate Automizer and the Search for Perfect Interpolants (Chapter)
Heizmann, M., Chen, Y. -F., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., . . . Podelski, A. (2018). Ultimate Automizer and the Search for Perfect Interpolants. In Unknown Book (Vol. 10806, pp. 447-451). doi:10.1007/978-3-319-89963-3_30DOI: 10.1007/978-3-319-89963-3_30
2017
A Novel Learning Algorithm for Buchi Automata Based on Family of DFAs and Classification Trees (Conference Paper)
Li, Y., Chen, Y. -F., Zhang, L., & Liu, D. (2017). A Novel Learning Algorithm for Buchi Automata Based on Family of DFAs and Classification Trees. In TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT I Vol. 10205 (pp. 208-226). doi:10.1007/978-3-662-54577-5_12DOI: 10.1007/978-3-662-54577-5_12
2016
Verify LTL with Fairness Assumptions Efficiently (Conference Paper)
Li, Y., Song, L., Feng, Y., & Zhang, L. (2016). Verify LTL with Fairness Assumptions Efficiently. In PROCEEDINGS 23RD INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING - TIME 2016 (pp. 41-50). doi:10.1109/TIME.2016.12DOI: 10.1109/TIME.2016.12
An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties (Conference Paper)
Li, Y., Liu, W., Turrini, A., Hahn, E. M., & Zhang, L. (2016). An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties. In DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS Vol. 9984 (pp. 280-296). doi:10.1007/978-3-319-47677-3_18DOI: 10.1007/978-3-319-47677-3_18
2015
A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking (Conference Paper)
van Dijk, T., Hahn, E. M., Jansen, D. N., Li, Y., Neele, T., Stoelinga, M., . . . Zhang, L. (2015). A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. In DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, SETTA 2015 Vol. 9409 (pp. 35-51). doi:10.1007/978-3-319-25942-0_3DOI: 10.1007/978-3-319-25942-0_3