This page on Google Scholar contains publications from other authors with the same name. See this DBLP entry for Lijun Zhang and yet this one for Lijun Zhang (this one contains publications from other authors with the same name).

Most of my papers can be downloaded below: Please respect the corresponding copyright by the publishers. For some papers, additional comments and corrections are marked (in red text) in the pdfs.

• 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.
• Probabilistic Preference Planning Problem for Markov Decision Processes, Li, M.; Turrini, A.; Hahn, E. M.; She, Z. and Zhang, L. In IEEE Trans. Software Eng., 48: 1545-1559, 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.
• Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification, Li, J.; Liu, J.; Yang, P.; Chen, L.; Huang, X. and Zhang, L. In SAS, pages 296-319, Springer, LNCS 11822, 2019.
• 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.
• An Axiomatisation of the Probabilistic μ-Calculus, Xu, J.; Liu, W.; Jansen, D. N. and Zhang, L. In ICFEM, pages 420-437, LNCS 11852, 2019.
• The Quest for Minimal Quotients for Probabilistic and Markov Automata, Eisentraut, C.; Hermanns, H.; Schuster, J.; Turrini, A. and Zhang, L. In Inf. Comput., 262: 162-186, 2018.
• Probabilistic Bisimulation for Realistic Schedulers, Zhang, L.; Yang, P.; Song, L.; Hermanns, H.; Eisentraut, C.; Jansen, D. N. and Godskesen, J. C. In Acta Informatica, 55: 461-488, 2018.
• 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.
• Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems, Fu, C.; Turrini, A.; Huang, X.; Song, L.; Feng, Y. and Zhang, L. In IJCAI, pages 4757-4763, ijcai.org, 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.
• Accelerating LTL satisfiability checking by SAT solvers, Li, J.; Pu, G.; Zhang, L.; Vardi, M. Y. and He, J. In J. Log. Comput., 28: 1011-1030, 2018.
• An explicit transition system construction approach to LTL satisfiability checking, Li, J.; Zhang, L.; Zhu, S.; Pu, G.; Vardi, M. Y. and He, J. In Formal Aspects Comput., 30: 193-217, 2018.
• An Automatic Proving Approach to Parameterized Verification, Li, Y.; Duan, K.; Jansen, D. N.; Pang, J.; Zhang, L.; Lv, Y. and Cai, S. In ACM Trans. Comput. Log., 19: 27:1-27:25, 2018.
• Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games, Hahn, E. M.; Schewe, S.; Turrini, A. and Zhang, L. In VMCAI, pages 266-287, LNCS 10145, 2017.
• 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.
• Distribution-Based Bisimulation for Labelled Markov Processes, Yang, P.; Jansen, D. N. and Zhang, L. In FORMATS, pages 170-186, LNCS 10419, 2017.
• On Equivalence Checking of Nondeterministic Finite Automata, Fu, C.; Deng, Y.; Jansen, D. N. and Zhang, L. In SETTA, pages 216-231, LNCS 10606, 2017.
• Finding Polynomial Loop Invariants for Probabilistic Programs, Feng, Y.; Zhang, L.; Jansen, D. N.; Zhan, N. and Xia, B. In ATVA, pages 400-416, LNCS 10482, 2017.
• Precisely deciding CSL formulas through approximate model checking for CTMCs, Feng, Y. and Zhang, L. In J. Comput. Syst. Sci., 89: 361-371, 2017.
• A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems, Wang, S.; Zhan, N. and Zhang, L. In Formal Asp. Comput., 29: 751-775, 2017.
• A Simple Algorithm for Solving Qualitative Probabilistic Parity Games, Hahn, E. M.; Schewe, S.; Turrini, A. and Zhang, L. In CAV, pages 291-311, LNCS 9780, 2016.
• Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes, He, F.; Gao, X.; Wang, M.; Wang, B.-Y. and Zhang, L. In ACM Trans. Softw. Eng. Methodol., 25: 21:1-21:39, 2016.
• 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.
• Efficient approximation of optimal control for continuous-time Markov games, Fearnley, J.; Rabe, M. N.; Schewe, S. and Zhang, L. In Inf. Comput., 247: 106-129, 2016.
• A space-efficient simulation algorithm on probabilistic automata, Zhang, L. and Jansen, D. N. In Inf. Comput., 249: 138-159, 2016.
• Multiphase until formulas over Markov reward models: An algebraic approach, Xu, M.; Zhang, L.; Jansen, D. N.; Zhu, H. and Yang, Z. In Theor. Comput. Sci., 611: 116-135, 2016.
• GPU-Accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs, Wu, Z.; Hahn, E. M.; Günay, A.; Zhang, L. and Liu, Y. In ECAI, pages 1726-1727, 2016.
• Lazy Probabilistic Model Checking without Determinisation, Hahn, E. M.; Li, G.; Schewe, S.; Turrini, A. and Zhang, L. In CONCUR, pages 354-367, LIPIcs 42, 2015.
• Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation, Chen, Y.-F.; Hong, C.-D.; Wang, B.-Y. and Zhang, L. In Computer Aided Verification (CAV), pages 658-674, Springer, 2015.
• A Simple Probabilistic Extension of Modal Mu-calculus, Liu, W.; Song, L.; Wang, J. and Zhang, L. In International Joint Conference on Artificial Intelligence (IJCAI), pages 882-888, AAAI Press, 2015.
• Planning for Stochastic Games with Co-safe Objectives, Song, L.; Feng, Y. and Zhang, L. In International Joint Conference on Artificial Intelligence (IJCAI), pages 1682-1688, AAAI Press, 2015.
• Decentralized Bisimulation for Multiagent Systems, Song, L.; Feng, Y. and Zhang, L. In International Conference on Autonomous Agents & Multiagent Systems (AAMAS), pages 209-217, ACM, 2015.
• A Nearly Optimal Upper Bound for the Self-Stabilization Time in Herman's Algorithm, Feng, Y. and Zhang, L. In Distributed Computing, 28: 233-244, 2015.
• Preference Planning for Markov Decision Processes, Li, M.; She, Z.; Turrini, A. and Zhang, L. In The Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI-15), pages 3313-3319, AAAI Press, 2015.
• Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems, He, F.; Gao, X.; Wang, B.-Y. and Zhang, L. In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL-15), pages 503-514, ACM, 2015.
• Incremental Bisimulation Abstraction Refinement, Song, L.; Zhang, L.; Hermanns, H. and Godskesen, J. C. In Transactions on Embedded Computing Systems (TECS), 13: 142:1-142:23, 2014.
• Probably safe or live, Katoen, J.-P.; Song, L. and Zhang, L. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, pages 55, ACM, 2014.
• A Nearly Optimal Upper Bound for the Self-Stabilization Time in Herman's Algorithm, Feng, Y. and Zhang, L. In Concurrency Theory - 25th International Conference (CONCUR 2014), pages 342-356, Springer, LNCS 8704, 2014.
• Aalta: an LTL satisfiability checker over Infinite/Finite traces, Li, J.; Yao, Y.; Pu, G.; Zhang, L. and He, J. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2014), pages 731-734, ACM, 2014.
• LTLf Satisfiability Checking, Li, J.; Zhang, L.; Pu, G.; Vardi, M. Y. and He, J. In 21st European Conference on Artificial Intelligence - Including Prestigious Applications of Intelligent Systems (ECAI 2014), pages 513-518, IOS Press, Frontiers in Artificial Intelligence and Applications 263, 2014.
• IscasMC: A Web-Based Probabilistic Model Checker, Hahn, E. M.; Li, Y.; Schewe, S.; Turrini, A. and Zhang, L. In Nineteenth international symposium of the Formal Methods Europe association (FM), pages 312-317, Springer, Lecture Notes in Computer Science 8442, 2014.
• When Equivalence and Bisimulation Join Forces in Probabilistic Automata, Feng, Y. and Zhang, L. In Nineteenth international symposium of the Formal Methods Europe association (FM), Springer, Lecture Notes in Computer Science , 2014.
• Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes, Song, L.; Zhang, L. and Godskesen, J. C. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference (VMCAI), pages 98-117, Springer, Lecture Notes in Computer Science 8318, 2014.
• Model Checking CSL for Markov Population Models, Spieler, D.; Hahn, E. M. and Zhang, L. In QAPL, pages 93-107, 2014.
• LTL Satisfiability Checking Revisited, Li, J.; Zhang, L.; Pu, G.; Vardi, M. and He, J. In 20th International Symposium on Temporal Representation and Reasoning (TIME), IEEE Comp. Society Press, 2013.
• Model Repair for Markov Decision Processes, Chen, T.; Hahn, E. M.; Han, T.; Kwiatkowska, M.; Qu, H. and Zhang, L. In Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 85-92, IEEE, 2013.
• Incremental Bisimulation Abstraction Refinement, Song, L.; Zhang, L.; Hermanns, H. and Godskesen, J. C. In 13th International Conference on Application of Concurrency to System Design (ACSD), pages 11-20, IEEE, 2013.
• A Semantics for Every GSPN, Eisentraut, C.; Hermanns, H.; Katoen, J.-P. and Zhang, L. In Application and Theory of Petri Nets and Concurrency - 34th International Conference (PETRI NETS), pages 90-109, Springer, Lecture Notes in Computer Science 7927, 2013.
• CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains, Gao, Y.; Hahn, E. M.; Zhan, N. and Zhang, L. In Automated Technology for Verification and Analysis - 11th International Symposium (ATVA), pages 464-468, Springer, Lecture Notes in Computer Science 8172, 2013.
• On the Relationship between LTL Normal Forms and Büchi Automata, Li, J.; Pu, G.; Zhang, L.; Wang, Z.; He, J. and Larsen, K. G. In Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, pages 256-270, Springer, Lecture Notes in Computer Science 8051, 2013.
• Deciding Bisimilarities on Distributions, Eisentraut, C.; Hermanns, H.; Krämer, J.; Turrini, A. and Zhang, L. In Quantitative Evaluation of Systems - 10th International Conference (QEST), pages 72-88, Springer, Lecture Notes in Computer Science 8054, 2013.
• Revisiting Weak Simulation for Substochastic Markov Chains, Jansen, D. N.; Song, L. and Zhang, L. In Quantitative Evaluation of Systems - 10th International Conference (QEST), pages 209-224, Springer, Lecture Notes in Computer Science 8054, 2013.
• Bisimulations Meet PCTL Equivalences for Probabilistic Automata, Song, L.; Zhang, L.; Godskesen, J. C. and Nielson, F. In Logical Methods in Computer Science, 9, 2013.
• A Tighter Bound for the Self-Stabilization Time in Herman's Algorithm, Feng, Y. and Zhang, L. In Information Processing Letters, 113: 486-488, 2013.
• The Quest for Minimal Quotients for Probabilistic Automata, Eisentraut, C.; Hermanns, H.; Schuster, J.; Turrini, A. and Zhang, L. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference (TACAS), pages 16-31, Springer, Lecture Notes in Computer Science 7795, 2013.
• Model Checking Conditional CSL for Continuous-Time Markov Chains, Gao, Y.; Xu, M.; Zhan, N. and Zhang, L. In Information Processing Letters, 113: 44-50, 2013.
• Efficient CSL Model Checking Using Stratification, Zhang, L.; Jansen, D. N.; Nielson, F. and Hermanns, H. In Logical Methods in Computer Science, 8, 2012.
• Safety Verification for Probabilistic Hybrid Systems, Zhang, L.; She, Z.; Ratschan, S.; Hermanns, H. and Hahn, E. M. In European Journal of Control, 18: 572-587, 2012.
• A General Framework for Probabilistic Characterizing Formulae, Sack, J. and Zhang, L. In Verification, Model Checking, and Abstract Interpretation - 13th International Conference (VMCAI), pages 396-411, Springer, Lecture Notes in Computer Science 7148, 2012.
• Belief Bisimulation for Hidden Markov Models - Logical Characterisation and Decision Algorithm, Jansen, D. N.; Nielson, F. and Zhang, L. In NASA Formal Methods - 4th International Symposium (NFM), pages 326-340, Springer, Lecture Notes in Computer Science 7226, 2012.
• Probabilistic Logical Characterization, Hermanns, H.; Parma, A.; Segala, R.; Wachter, B. and Zhang, L. In Information and Computation, 209: 154-172, 2011.
• From Concurrency Models to Numbers -- Performance and Dependability, Hermanns, H. and Zhang, L. In Software and Systems Safety, pages 182-210, IOS Press, NATO Science for Peace and Security Series - D: Information and Communication Security 30, 2011.
• Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems, Hahn, E. M.; Norman, G.; Parker, D.; Wachter, B. and Zhang, L. In Eighth International Conference on Quantitative Evaluation of Systems (QEST), pages 69-78, IEEE Computer Society, 2011.
• On Stabilization in Herman's Algorithm, Kiefer, S.; Murawski, A. S.; Ouaknine, J.; Worrell, J. and Zhang, L. In Automata, Languages and Programming - 38th International Colloquium (ICALP), pages 466-477, Springer, Lecture Notes in Computer Science 6756, 2011.
• Automata-Based CSL Model Checking, Zhang, L.; Jansen, D. N.; Nielson, F. and Hermanns, H. In Automata, Languages and Programming - 38th International Colloquium (ICALP), pages 271-282, Springer, Lecture Notes in Computer Science 6756, 2011.
• Synthesis for PCTL in Parametric Markov Decision Processes, Hahn, E. M.; Han, T. and Zhang, L. In NASA Formal Methods - Third International Symposium (NFM), pages 146-161, Springer, Lecture Notes in Computer Science 6617, 2011.
• Model Checking Algorithms for CTMDPs, Buchholz, P.; Hahn, E. M.; Hermanns, H. and Zhang, L. In Computer Aided Verification - 23rd International Conference (CAV), pages 225-242, Springer, Lecture Notes in Computer Science 6806, 2011.
• Measurability and safety verification for stochastic hybrid systems, Fränzle, M.; Hahn, E. M.; Hermanns, H.; Wolovick, N. and Zhang, L. In Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pages 43-52, ACM, 2011.
• Bisimulations Meet PCTL Equivalences for Probabilistic Automata, Song, L.; Zhang, L. and Godskesen, J. C. In Concurrency Theory, 22nd International Conference (CONCUR), pages 108-123, Springer, Lecture Notes in Computer Science 6901, 2011.
• Efficient Approximation of Optimal Control for Continuous-Time Markov Games, Fearnley, J.; Rabe, M.; Schewe, S. and Zhang, L. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 399-410, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, LIPIcs 13, 2011.
• Probabilistic Reachability for Parametric Markov Models, Hahn, E. M.; Hermanns, H. and Zhang, L. In STTT, 13: 3-19, 2011.
• On Probabilistic Automata in Continuous Time, Eisentraut, C.; Hermanns, H. and Zhang, L. In 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 342-351, IEEE CS Press, 2010.
• Concurrency and Composition in a Stochastic World, Eisentraut, C.; Hermanns, H. and Zhang, L. In Concurrency Theory, 21th International Conference (CONCUR), pages 21-39, Springer, Lecture Notes in Computer Science 6269, 2010.
• PARAM: A Model Checker for Parametric Markov Models, Hahn, E. M.; Hermanns, H.; Wachter, B. and Zhang, L. In Computer Aided Verification, 22nd International Conference (CAV), pages 660-664, Springer, Lecture Notes in Computer Science 6174, 2010.
• Safety Verification for Probabilistic Hybrid Systems, Zhang, L.; She, Z.; Ratschan, S.; Hermanns, H. and Hahn, E. M. In Computer Aided Verification, 22nd International Conference (CAV), pages 196-211, Springer, Lecture Notes in Computer Science 6174, 2010.
• Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains, Calin, G.; Crouzen, P.; D'Argenio, P. R.; Hahn, E. M. and Zhang, L. In Model Checking Software - 17th International SPIN Workshop, pages 193-211, Springer, Lecture Notes in Computer Science 6349, 2010.
• Model Checking Interactive Markov Chains, Zhang, L. and Neuhäusser, M. R. In Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference (TACAS), pages 53-68, Springer, Lecture Notes in Computer Science 6015, 2010.
• PASS: Abstraction Refinement for Infinite Probabilistic Models, Hahn, E. M.; Hermanns, H.; Wachter, B. and Zhang, L. In Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference (TACAS), pages 353-357, Springer, Lecture Notes in Computer Science 6015, 2010.
• Best Probabilistic Transformers, Wachter, B. and Zhang, L. In Verification, Model Checking, and Abstract Interpretation, 11th International Conference (VMCAI), pages 362-379, Springer, Lecture Notes in Computer Science 5944, 2010.
• INFAMY: An Infinite-State Markov Model Checker, Hahn, E. M.; Hermanns, H.; Wachter, B. and Zhang, L. In Computer Aided Verification, 21st International Conference (CAV), pages 641-647, Springer, Lecture Notes in Computer Science 5643, 2009.
• Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains, Hahn, E. M.; Hermanns, H.; Wachter, B. and Zhang, L. In Fundamenta Informaticae, 95: 129-155, 2009.
• FlowSim Simulation Benchmarking Platform, Bogdoll, J.; Hermanns, H. and Zhang, L. In Sixth International Conference on the Quantitative Evaluation of Systems (QEST), pages 211-212, IEEE Computer Society, 2009.
• Probabilistic Reachability for Parametric Markov Models, Hahn, E. M.; Hermanns, H. and Zhang, L. In Model Checking Software, 16th International SPIN Workshop, pages 88-106, Springer, Lecture Notes in Computer Science 5578, 2009.
• Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations, Zhang, L.; Hermanns, H.; Eisenbrand, F. and Jansen, D. N. In Logical Methods in Computer Science, 4, 2008.
• Time-bounded model checking of infinite-state continuous-time Markov chains, Zhang, L.; Hermanns, H.; Hahn, E. M. and Wachter, B. In 8th International Conference on Application of Concurrency to System Design (ACSD), pages 98-107, IEEE, 2008.
• Probabilistic CEGAR, Hermanns, H.; Wachter, B. and Zhang, L. In Computer Aided Verification, 20th International Conference (CAV), pages 162-175, Springer, Lecture Notes in Computer Science 5123, 2008.
• A Space-Efficient Probabilistic Simulation Algorithm, Zhang, L. In Concurrency Theory, 19th International Conference (CONCUR), pages 248-263, Springer, Lecture Notes in Computer Science 5201, 2008.
• On the Minimisation of Acyclic Models, Crouzen, P.; Hermanns, H. and Zhang, L. In Concurrency Theory, 19th International Conference (CONCUR), pages 295-309, Springer, Lecture Notes in Computer Science 5201, 2008.
• An Experimental Evaluation of Probabilistic Simulation, Bogdoll, J.; Hermanns, H. and Zhang, L. In Formal Techniques for Networked and Distributed Systems (FORTE), pages 37-52, Springer, Lecture Notes in Computer Science 5048, 2008.
• Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations, Zhang, L.; Hermanns, H.; Eisenbrand, F. and Jansen, D. N. In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference (TACAS), pages 155-169, Springer, Lecture Notes in Computer Science 4424, 2007.
• Deciding Simulations on Probabilistic Automata, Zhang, L. and Hermanns, H. In Automated Technology for Verification and Analysis, 5th International Symposium (ATVA), pages 207-222, Springer, Lecture Notes in Computer Science 4762, 2007.
• Probabilistic Model Checking Modulo Theories, Wachter, B.; Zhang, L. and Hermanns, H. In Fourth International Conference on the Quantitative Evaluaiton of Systems (QEST), pages 129-140, IEEE Computer Society, 2007.
• Logic and Model Checking for Hidden Markov Models, Zhang, L.; Hermanns, H. and Jansen, D. N. In Formal Techniques for Networked and Distributed Systems (FORTE), pages 98-112, Springer, Lecture Notes in Computer Science 3731, 2005.