Trustworthy Intelligent Systems

Lijun Zhang (张立军)'s Publications

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 PDF.

  • Weizhi Feng, Yicheng Liu, Jiaxiang Liu, David N. Jansen, Lijun Zhang, Zhilin Wu (): Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once. In 61st ACM/IEEE Design Automation Conference, DAC 2024, San Francisco, CA, USA, June 23-27, 2024, 2024.
  • Deqian Yang, Hui Meng, Haochen Zhao, Gaojie Jin, Lijun Zhang: Class-aware Cross Pseudo Supervision Framework for Semi-Supervised Multi-Organ Segmentation in Abdominal CT Scans. In Patter Recognition and Computer Vision - 7th Chinese Conference, PRCV 2024, 2024. BIB
  • Lijia Yu, Xiao-Shan Gao, Lijun Zhang: Optimal Robust Memorization with ReLU Neural Networks. In The Twelfth International Conference on Learning Representations (ICLR), 2024. URL BIB
  • Lijia Yu, Shuang Liu, Yibo Miao, Lijun Zhang, Xiaoshan Gao: Generalization Bound and New Algorithm for Clean-Label Backdoor Attack. In International Conference on Machine Learning, ICML 2024, 21-27 July 2024, Vienna, Austria, 2024. BIB
  • 刘颖, 杨鹏飞, 张立军, 吴志林 (), 冯元 (): 前馈神经网络和循环神经网络的鲁棒性验证综述. In 软件学报 34(7):3134, 2023. DOI BIB
  • Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y. Vardi (), Lijun Zhang: On the power of finite ambiguity in Büchi complementation. In Inf. Comput. 292:105032, 2023. DOI BIB
  • Jianling Fu, Cheng-Chao Huang, Yong Li, Jingyi Mei, Ming Xu, Lijun Zhang: Quantitative controller synthesis for consumption Markov decision processes. In Inf. Process. Lett. 180:106342, 2023. DOI BIB
  • Chen Fu, Andrea Turrini, Xiaowei Huang (), Lei Song, Yuan Feng (), Lijun Zhang: Model Checking for Probabilistic Multiagent Systems. In Journal of Computer Science and Technology 38(4):1-25, 2023. DOI BIB
  • Ying Liu, Andrea Turrini, Ernst Moritz Hahn (), Bai Xue (), Lijun Zhang: Scenario Approach for Parametric Markov Models. 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 158-180, 2023. DOI BIB
  • Depeng Liu, Bow-Yaw Wang, Chen Fu, Lijun Zhang: Model checking differentially private properties. In Theor. Comput. Sci. 943:153-170, 2023. DOI BIB
  • Dejin Ren, Wanli Lu, Jidong Lv, Lijun Zhang, Bai Xue (): Model Predictive Control with Reach-avoid Analysis. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 5437-5445, 2023. DOI BIB
  • Liang Zhang, Nathaniel Xu, Pengfei Yang, Gaojie Jin, Cheng-Chao Huang, Lijun Zhang: TrajPAC: Towards Robustness Verification of Pedestrian Trajectory Prediction Models. In IEEE/CVF International Conference on Computer Vision, ICCV 2023, Paris, France, October 1-6, 2023, pages 8293-8305, 2023. DOI BIB
  • Chen Fu, Ernst Moritz Hahn (), Yong Li, Sven Schewe (), Meng Sun (), Andrea Turrini, Lijun Zhang: 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
  • Gaojie Jin, Xinping Yi, Pengfei Yang, Lijun Zhang, Sven Schewe (), Xiaowei Huang (): Weight Expansion: A New Perspective on Dropout and Generalization. In Trans. Mach. Learn. Res. 2022, 2022. URL BIB
  • Yi Li, Xie Li, Yong Li, Xuechao Sun, Andrea Turrini, Lijun Zhang: Synthesizing ranking functions for loop programs via SVM. In Theor. Comput. Sci. 935:1-20, 2022. DOI BIB
  • Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi (), Lijun Zhang: 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
  • Meilun Li, Andrea Turrini, Ernst Moritz Hahn (), Zhikun She, Lijun Zhang: Probabilistic Preference Planning Problem for Markov Decision Processes. In IEEE Trans. Software Eng. 48(5):1545-1559, 2022. DOI BIB
  • Renjue Li, Pengfei Yang, Cheng-Chao Huang, Youcheng Sun, Bai Xue (), Lijun Zhang: Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning. In 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022, pages 2189-2201, 2022. DOI BIB
  • Depeng Liu, Bow-Yaw Wang, Lijun Zhang: Verifying Pufferfish Privacy in Hidden Markov Models. 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 174-196, 2022. DOI BIB
  • Wanwei Liu, Junnan Xu, David N. Jansen, Andrea Turrini, Lijun Zhang: An Axiom System of Probabilistic Mu-Calculus. In Tsinghua Science and Technology 27(2):372-385, 2022. DOI BIB
  • Tomás Vojnar, Lijun Zhang: Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2019. In Int. J. Softw. Tools Technol. Transf. 24(1):29-31, 2022. DOI BIB
  • Shizhen Yu, Yifan Dong, Jiuyang Liu, Yong Li, Zhilin Wu (), David N. Jansen, Lijun Zhang: 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
  • Konstantin Kuznetsov, Chen Fu, Song Gao, David N. Jansen, Lijun Zhang, Andreas Zeller (): Frontmatter: mining Android user interfaces at scale. In ESEC/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Athens, Greece, August 23-28, 2021, pages 1580-1584, 2021. DOI BIB
  • Song Gao, Bohua Zhan (), Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen, Lijun Zhang: Formal Verification of Consensus in the Taurus Distributed Database. In Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 741-751, 2021. DOI BIB
  • Yong Li, Yu-Fang Chen (), Lijun Zhang, Depeng Liu: A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. In Inf. Comput. 281:104678, 2021. DOI BIB
  • Yong Li, Yih-Kuen Tsay (), Andrea Turrini, Moshe Y. Vardi (), Lijun Zhang: 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
  • Yong Li, Andrea Turrini, Moshe Y. Vardi (), Lijun Zhang: 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
  • Sven Schewe (), Lijun Zhang: Editorial - Special issue on Concurrency Theory (CONCUR 2018). In J. Comput. Syst. Sci. 119:19-20, 2021. DOI BIB
  • Bing Sun, Jun Sun (), Ting Dai, Lijun Zhang: Probabilistic Verification of Neural Networks Against Group Fairness. In Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 83-102, 2021. DOI BIB
  • Pengfei Yang, Jianlin Li (), Jiangchao Liu, Cheng-Chao Huang, Renjue Li, Liqian Chen, Xiaowei Huang (), Lijun Zhang: Enhancing Robustness Verification for Deep Neural Networks via Symbolic Propagation. In Formal Aspects Comput. 33(3):407-435, 2021. DOI BIB
  • Pengfei Yang, Renjue Li, Jianlin Li (), Cheng-Chao Huang, Jingyi Wang, Jun Sun (), Bai Xue (), Lijun Zhang: Improving Neural Network Verification through Spurious Region Guided Refinement. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 389-408, 2021. DOI BIB
  • Yong Li, Andrea Turrini, Xuechao Sun, Lijun Zhang: 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
  • Gaojie Jin, Xinping Yi, Liang Zhang, Lijun Zhang, Sven Schewe (), Xiaowei Huang (): How does Weight Correlation Affect Generalisation Ability of Deep Neural Networks?. In Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, 2020. URL BIB
  • Renjue Li, Jianlin Li (), Cheng-Chao Huang, Pengfei Yang, Xiaowei Huang (), Lijun Zhang, Bai Xue (), Holger Hermanns (): PRODeep: a platform for robustness verification of deep neural networks. 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 1630-1634, 2020. DOI BIB
  • Xie Li, Yi Li, Yong Li, Xuechao Sun, Andrea Turrini, Lijun Zhang: 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
  • Yong Li, Moshe Y. Vardi (), Lijun Zhang: 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
  • Jianlin Li (), Jiangchao Liu, Pengfei Yang, Liqian Chen, Xiaowei Huang (), Lijun Zhang: Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification. In Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, volume 11822 of Lecture Notes in Computer Science, pages 296-319, 2019. DOI BIB
  • Yi Li, Xuechao Sun, Yong Li, Andrea Turrini, Lijun Zhang: 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
  • Jianwen Li, Shufang Zhu, Geguang Pu, Lijun Zhang, Moshe Y. Vardi (): SAT-based explicit LTL reasoning and its application to satisfiability checking. In Formal Methods Syst. Des. 54(2):164-190, 2019. DOI BIB
  • Junnan Xu, Wanwei Liu, David N. Jansen, Lijun Zhang: An Axiomatisation of the Probabilistic μ-Calculus. 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 420-437, 2019. DOI BIB
  • Yu-Fang Chen (), Matthias Heizmann, Ondrej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang: 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
  • Christian Eisentraut, Holger Hermanns (), Johann Schuster, Andrea Turrini, Lijun Zhang: The quest for minimal quotients for probabilistic and Markov automata. In Inf. Comput. 262:162-186, 2018. DOI BIB
  • Bernd Finkbeiner, Geguang Pu, Lijun Zhang: Preface for the special issue for ATVA 2015. In Acta Informatica 55(8):625-626, 2018. DOI BIB
  • Chen Fu, Andrea Turrini, Xiaowei Huang (), Lei Song, Yuan Feng (), Lijun Zhang: Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 4757-4763, 2018. DOI BIB
  • Yongjian Li, Kaiqiang Duan, David N. Jansen, Jun Pang, Lijun Zhang, Yi Lv, Shaowei Cai: An Automatic Proving Approach to Parameterized Verification. In ACM Trans. Comput. Log. 19(4):27:1-27:25, 2018. DOI BIB
  • Jianwen Li, Geguang Pu, Lijun Zhang, Moshe Y. Vardi (), Jifeng He: Accelerating LTL satisfiability checking by SAT solvers. In J. Log. Comput. 28(6):1011-1030, 2018. DOI BIB
  • Yong Li, Andrea Turrini, Yu-Fang Chen (), Lijun Zhang: 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
  • Yong Li, Andrea Turrini, Lijun Zhang, Sven Schewe (): 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
  • Jianwen Li, Lijun Zhang, Shufang Zhu, Geguang Pu, Moshe Y. Vardi (), Jifeng He: An explicit transition system construction approach to LTL satisfiability checking. In Formal Aspects Comput. 30(2):193-217, 2018. DOI BIB
  • Depeng Liu, Bow-Yaw Wang, Lijun Zhang: Model Checking Differentially Private Properties. In Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, volume 11275 of Lecture Notes in Computer Science, pages 394-414, 2018. DOI BIB
  • Lijun Zhang, Pengfei Yang, Lei Song, Holger Hermanns (), Christian Eisentraut, David N. Jansen, Jens Chr. Godskesen: Probabilistic bisimulation for realistic schedulers. In Acta Informatica 55(6):461-488, 2018. DOI BIB
  • Yuan Feng (), Lijun Zhang: Precisely deciding CSL formulas through approximate model checking for CTMCs. In J. Comput. Syst. Sci. 89:361-371, 2017. DOI BIB
  • Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan (), Bican Xia: Finding Polynomial Loop Invariants for Probabilistic Programs. In Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings, volume 10482 of Lecture Notes in Computer Science, pages 400-416, 2017. DOI BIB
  • Chen Fu, Yuxin Deng (), David N. Jansen, Lijun Zhang: On Equivalence Checking of Nondeterministic Finite Automata. In Dependable Software Engineering. Theories, Tools, and Applications - Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings, volume 10606 of Lecture Notes in Computer Science, pages 216-231, 2017. DOI BIB
  • Ernst Moritz Hahn (), Sven Schewe (), Andrea Turrini, Lijun Zhang: Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, volume 10145 of Lecture Notes in Computer Science, pages 266-287, 2017. DOI BIB
  • Yong Li, Yu-Fang Chen (), Lijun Zhang, Depeng Liu: 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
  • Shuling Wang, Naijun Zhan (), Lijun Zhang: A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems. In Formal Aspects Comput. 29(4):751-775, 2017. DOI BIB
  • Pengfei Yang, David N. Jansen, Lijun Zhang: Distribution-Based Bisimulation for Labelled Markov Processes. In Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings, volume 10419 of Lecture Notes in Computer Science, pages 170-186, 2017. DOI BIB
  • John Fearnley, Markus N. Rabe, Sven Schewe (), Lijun Zhang: Efficient approximation of optimal control for continuous-time Markov games. In Inf. Comput. 247:106-129, 2016. DOI BIB
  • Ernst Moritz Hahn (), Sven Schewe (), Andrea Turrini, Lijun Zhang: A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, volume 9780 of Lecture Notes in Computer Science, pages 291-311, 2016. DOI BIB
  • Fei He (), Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, Lijun Zhang: Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes. In ACM Trans. Softw. Eng. Methodol. 25(3):21:1-21:39, 2016. DOI BIB
  • Yong Li, Wanwei Liu, Andrea Turrini, Ernst Moritz Hahn (), Lijun Zhang: 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
  • Yong Li, Lei Song, Yuan Feng (), Lijun Zhang: 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
  • Zhimin Wu, Ernst Moritz Hahn (), Akin Günay, Lijun Zhang, Yang Liu: GPU-Accelerated Value Iteration for the Computation of Reachability Probabilities in MDPs. In ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016),, volume 285 of Frontiers in Artificial Intelligence and Applications, pages 1726-1727, 2016. DOI BIB
  • Ming Xu, Lijun Zhang, David N. Jansen, Huibiao Zhu, Zongyuan Yang: Multiphase until formulas over Markov reward models: An algebraic approach. In Theor. Comput. Sci. 611:116-135, 2016. DOI BIB
  • Lijun Zhang, David N. Jansen: A space-efficient simulation algorithm on probabilistic automata. In Inf. Comput. 249:138-159, 2016. DOI BIB
  • Yu-Fang Chen (), Chih-Duo Hong, Bow-Yaw Wang, Lijun Zhang: Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 658-674, 2015. DOI BIB
  • Tom van Dijk (), Ernst Moritz Hahn (), David N. Jansen, Yong Li, Thomas Neele (), Mariëlle Stoelinga (), Andrea Turrini, Lijun Zhang: 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
  • Christian Eisentraut, Jens Chr. Godskesen, Holger Hermanns (), Lei Song, Lijun Zhang: Probabilistic Bisimulation for Realistic Schedulers. In FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 248-264, 2015. DOI BIB
  • Yuan Feng (), Lijun Zhang: A nearly optimal upper bound for the self-stabilization time in Herman's algorithm. In Distributed Comput. 28(4):233-244, 2015. DOI BIB
  • Yuan Feng (), Ernst Moritz Hahn (), Andrea Turrini, Lijun Zhang: QPMC: A Model Checker for Quantum Programs and Protocols. In FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 265-272, 2015. DOI BIB
  • Ernst Moritz Hahn (), Guangyuan Li, Sven Schewe (), Andrea Turrini, Lijun Zhang: Lazy Probabilistic Model Checking without Determinisation. In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 354-367, 2015. DOI BIB
  • Fei He (), Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang: Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 503-514, 2015. DOI BIB
  • Meilun Li, Zhikun She, Andrea Turrini, Lijun Zhang: Preference Planning for Markov Decision Processes. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA, pages 3313-3319, 2015. DOI BIB
  • Wanwei Liu, Lei Song, Ji Wang, Lijun Zhang: A Simple Probabilistic Extension of Modal Mu-calculus. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 882-888, 2015. URL BIB
  • Yu Peng, Shuling Wang, Naijun Zhan (), Lijun Zhang: Extending Hybrid CSP with Probability and Stochasticity. 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 87-102, 2015. DOI BIB
  • Lei Song, Yuan Feng (), Lijun Zhang: Decentralized Bisimulation for Multiagent Systems. In Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015, pages 209-217, 2015. URL BIB
  • Lei Song, Yuan Feng (), Lijun Zhang: Planning for Stochastic Games with Co-Safe Objectives. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 1682-1688, 2015. URL BIB
  • Yuan Feng (), Lijun Zhang: A Nearly Optimal Upper Bound for the Self-Stabilization Time in Herman's Algorithm. In CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, volume 8704 of Lecture Notes in Computer Science, pages 342-356, 2014. DOI BIB
  • Yuan Feng (), Lijun Zhang: When Equivalence and Bisimulation Join Forces in Probabilistic Automata. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 247-262, 2014. DOI BIB
  • Ernst Moritz Hahn (), Yi Li, Sven Schewe (), Andrea Turrini, Lijun Zhang: IscasMc: A Web-Based Probabilistic Model Checker. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 312-317, 2014. DOI BIB
  • Joost-Pieter Katoen (), Lei Song, Lijun Zhang: Probably safe or live. 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 '14, Vienna, Austria, July 14 - 18, 2014, pages 55:1-55:10, 2014. DOI BIB
  • Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi (), Jifeng He: LTLf Satisfiability Checking. In ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014), volume 263 of Frontiers in Artificial Intelligence and Applications, pages 513-518, 2014. DOI BIB
  • Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang, Jifeng He: Aalta: an LTL satisfiability checker over Infinite/Finite traces. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16 - 22, 2014, pages 731-734, 2014. DOI BIB
  • Lei Song, Lijun Zhang, Jens Chr. Godskesen: Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings, volume 8318 of Lecture Notes in Computer Science, pages 98-117, 2014. DOI BIB
  • Lei Song, Lijun Zhang, Holger Hermanns (), Jens Chr. Godskesen: Incremental Bisimulation Abstraction Refinement. In ACM Trans. Embed. Comput. Syst. 13(4s):142:1-142:23, 2014. DOI BIB
  • David Spieler, Ernst Moritz Hahn (), Lijun Zhang: Model Checking CSL for Markov Population Models. In Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble, France, 12-13 April 2014, volume 154 of EPTCS, pages 93-107, 2014. DOI BIB
  • Taolue Chen (), Ernst Moritz Hahn (), Tingting Han, Marta Z. Kwiatkowska, Hongyang Qu, Lijun Zhang: Model Repair for Markov Decision Processes. In Seventh International Symposium on Theoretical Aspects of Software Engineering, TASE 2013, 1-3 July 2013, Birmingham, UK, pages 85-92, 2013. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Joost-Pieter Katoen (), Lijun Zhang: A Semantics for Every GSPN. In Application and Theory of Petri Nets and Concurrency - 34th International Conference, PETRI NETS 2013, Milan, Italy, June 24-28, 2013. Proceedings, volume 7927 of Lecture Notes in Computer Science, pages 90-109, 2013. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Julia Krämer, Andrea Turrini, Lijun Zhang: Deciding Bisimilarities on Distributions. In Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8054 of Lecture Notes in Computer Science, pages 72-88, 2013. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Johann Schuster, Andrea Turrini, Lijun Zhang: The Quest for Minimal Quotients for Probabilistic Automata. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7795 of Lecture Notes in Computer Science, pages 16-31, 2013. DOI BIB
  • Yuan Feng (), Lijun Zhang: A tighter bound for the self-stabilization time in Herman's algorithm. In Inf. Process. Lett. 113(13):486-488, 2013. DOI BIB
  • Yang Gao, Ernst Moritz Hahn (), Naijun Zhan (), Lijun Zhang: CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, volume 8172 of Lecture Notes in Computer Science, pages 464-468, 2013. DOI BIB
  • Yang Gao, Ming Xu, Naijun Zhan (), Lijun Zhang: Model checking conditional CSL for continuous-time Markov chains. In Inf. Process. Lett. 113(1-2):44-50, 2013. DOI BIB
  • David N. Jansen, Lei Song, Lijun Zhang: Revisiting Weak Simulation for Substochastic Markov Chains. In Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8054 of Lecture Notes in Computer Science, pages 209-224, 2013. DOI BIB
  • Jianwen Li, Geguang Pu, Lijun Zhang, Zheng Wang, Jifeng He, Kim Guldstrand Larsen: On the Relationship between LTL Normal Forms and Büchi Automata. In Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, volume 8051 of Lecture Notes in Computer Science, pages 256-270, 2013. DOI BIB
  • Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi (), Jifeng He: LTL Satisfiability Checking Revisited. In 2013 20th International Symposium on Temporal Representation and Reasoning, Pensacola, FL, USA, September 26-28, 2013, pages 91-98, 2013. DOI BIB
  • Lei Song, Lijun Zhang, Holger Hermanns (), Jens Chr. Godskesen: Incremental Bisimulation Abstraction Refinement. In 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, 8-10 July, 2013, pages 11-20, 2013. DOI BIB
  • Lei Song, Lijun Zhang, Jens Chr. Godskesen: Bisimulations Meet PCTL Equivalences for Probabilistic Automata. In Log. Methods Comput. Sci. 9(2), 2013. DOI BIB
  • Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns (), Ernst Moritz Hahn (): Safety Verification for Probabilistic Hybrid Systems. In Eur. J. Control 18(6):572-587, 2012. DOI BIB
  • David N. Jansen, Flemming Nielson, Lijun Zhang: Belief Bisimulation for Hidden Markov Models - Logical Characterisation and Decision Algorithm. In NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings, volume 7226 of Lecture Notes in Computer Science, pages 326-340, 2012. DOI BIB
  • Joshua Sack, Lijun Zhang: A General Framework for Probabilistic Characterizing Formulae. In Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings, volume 7148 of Lecture Notes in Computer Science, pages 396-411, 2012. DOI BIB
  • Peter Buchholz, Ernst Moritz Hahn (), Holger Hermanns (), Lijun Zhang: Model Checking Algorithms for CTMDPs. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 225-242, 2011. DOI BIB
  • John Fearnley, Markus N. Rabe, Sven Schewe (), Lijun Zhang: Efficient Approximation of Optimal Control for Continuous-Time Markov Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India, volume 13 of LIPIcs, pages 399-410, 2011. DOI BIB
  • Martin Fränzle, Ernst Moritz Hahn (), Holger Hermanns (), Nicolás Wolovick, Lijun Zhang: Measurability and safety verification for stochastic hybrid systems. In Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011, pages 43-52, 2011. DOI BIB
  • Ernst Moritz Hahn (), Holger Hermanns (), Lijun Zhang: Probabilistic reachability for parametric Markov models. In Int. J. Softw. Tools Technol. Transf. 13(1):3-19, 2011. DOI BIB
  • Ernst Moritz Hahn (), Tingting Han, Lijun Zhang: Synthesis for PCTL in Parametric Markov Decision Processes. In NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, volume 6617 of Lecture Notes in Computer Science, pages 146-161, 2011. DOI BIB
  • Ernst Moritz Hahn (), Gethin Norman, David Parker, Björn Wachter, Lijun Zhang: Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems. In Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5-8 September, 2011, pages 69-78, 2011. DOI BIB
  • Holger Hermanns (), Augusto Parma, Roberto Segala, Björn Wachter, Lijun Zhang: Probabilistic Logical Characterization. In Inf. Comput. 209(2):154-172, 2011. DOI BIB
  • Holger Hermanns (), Lijun Zhang: From Concurrency Models to Numbers - Performance and Dependability. In Software and Systems Safety - Specification and Verification, volume 30 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 182-210, 2011. DOI BIB
  • Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, James Worrell, Lijun Zhang: On Stabilization in Herman's Algorithm. In Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 466-477, 2011. DOI BIB
  • Lei Song, Lijun Zhang, Jens Chr. Godskesen: Bisimulations Meet PCTL Equivalences for Probabilistic Automata. In CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 108-123, 2011. DOI BIB
  • Lijun Zhang, David N. Jansen, Flemming Nielson, Holger Hermanns (): Automata-Based CSL Model Checking. In Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 271-282, 2011. DOI BIB
  • Lijun Zhang, David N. Jansen, Flemming Nielson, Holger Hermanns (): Automata-Based CSL Model Checking. In Log. Methods Comput. Sci. 8(2), 2011. DOI BIB
  • Georgel Calin, Pepijn Crouzen, Pedro R. D'Argenio, Ernst Moritz Hahn (), Lijun Zhang: Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains. In Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings, volume 6349 of Lecture Notes in Computer Science, pages 193-211, 2010. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Lijun Zhang: Concurrency and Composition in a Stochastic World. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 21-39, 2010. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Lijun Zhang: On Probabilistic Automata in Continuous Time. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 342-351, 2010. DOI BIB
  • Ernst Moritz Hahn (), Holger Hermanns (), Björn Wachter, Lijun Zhang: PARAM: A Model Checker for Parametric Markov Models. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 660-664, 2010. DOI BIB
  • Ernst Moritz Hahn (), Holger Hermanns (), Björn Wachter, Lijun Zhang: PASS: Abstraction Refinement for Infinite Probabilistic Models. In Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 353-357, 2010. DOI BIB
  • Martin R. Neuhäußer, Lijun Zhang: Time-Bounded Reachability Probabilities in Continuous-Time Markov Decision Processes. In QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010, pages 209-218, 2010. DOI BIB
  • Björn Wachter, Lijun Zhang: Best Probabilistic Transformers. In Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings, volume 5944 of Lecture Notes in Computer Science, pages 362-379, 2010. DOI BIB
  • Lijun Zhang, Martin R. Neuhäußer: Model Checking Interactive Markov Chains. In Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 53-68, 2010. DOI BIB
  • Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns (), Ernst Moritz Hahn (): Safety Verification for Probabilistic Hybrid Systems. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 196-211, 2010. DOI BIB
  • Jonathan Bogdoll, Holger Hermanns (), Lijun Zhang: FlowSim Simulation Benchmarking Platform. In QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, Budapest, Hungary, 13-16 September 2009, pages 211-212, 2009. DOI BIB
  • Ernst Moritz Hahn (), Holger Hermanns (), Björn Wachter, Lijun Zhang: Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains. In Fundam. Informaticae 95(1):129-155, 2009. DOI BIB
  • Ernst Moritz Hahn (), Holger Hermanns (), Björn Wachter, Lijun Zhang: INFAMY: An Infinite-State Markov Model Checker. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 641-647, 2009. DOI BIB
  • Ernst Moritz Hahn (), Holger Hermanns (), Lijun Zhang: Probabilistic Reachability for Parametric Markov Models. In Model Checking Software, 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings, volume 5578 of Lecture Notes in Computer Science, pages 88-106, 2009. DOI BIB
  • Jonathan Bogdoll, Holger Hermanns (), Lijun Zhang: An Experimental Evaluation of Probabilistic Simulation. In Formal Techniques for Networked and Distributed Systems - FORTE 2008, 28th IFIP WG 6.1 International Conference, Tokyo, Japan, June 10-13, 2008, Proceedings, volume 5048 of Lecture Notes in Computer Science, pages 37-52, 2008. DOI BIB
  • Pepijn Crouzen, Holger Hermanns (), Lijun Zhang: On the Minimisation of Acyclic Models. In CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings, volume 5201 of Lecture Notes in Computer Science, pages 295-309, 2008. DOI BIB
  • Holger Hermanns (), Björn Wachter, Lijun Zhang: Probabilistic CEGAR. In Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, volume 5123 of Lecture Notes in Computer Science, pages 162-175, 2008. DOI BIB
  • Lijun Zhang: A Space-Efficient Probabilistic Simulation Algorithm. In CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings, volume 5201 of Lecture Notes in Computer Science, pages 248-263, 2008. DOI BIB
  • Lijun Zhang, Holger Hermanns (), Friedrich Eisenbrand, David N. Jansen: Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. In Log. Methods Comput. Sci. 4(4), 2008. DOI BIB
  • Lijun Zhang, Holger Hermanns (), Ernst Moritz Hahn (), Björn Wachter: Time-bounded model checking of infinite-state continuous-time Markov chains. In 8th International Conference on Application of Concurrency to System Design (ACSD 2008), Xi'an, China, June 23-27, 2008, pages 98-107, 2008. DOI BIB
  • Björn Wachter, Lijun Zhang, Holger Hermanns (): Probabilistic Model Checking Modulo Theories. In Fourth International Conference on the Quantitative Evaluaiton of Systems (QEST 2007), 17-19 September 2007, Edinburgh, Scotland, UK, pages 129-140, 2007. DOI BIB
  • Lijun Zhang, Holger Hermanns (): Deciding Simulations on Probabilistic Automata. In Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings, volume 4762 of Lecture Notes in Computer Science, pages 207-222, 2007. DOI BIB
  • Lijun Zhang, Holger Hermanns (), Friedrich Eisenbrand, David N. Jansen: Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4424 of Lecture Notes in Computer Science, pages 155-169, 2007. DOI BIB
  • Irene Eusgeld, Bernhard Fechner, Felix Salfner, Max Walter, Philipp Limbourg, Lijun Zhang: Hardware Reliability. In Dependability Metrics: Advanced Lectures [result from a Dagstuhl seminar, October 30 - November 1, 2005], volume 4909 of Lecture Notes in Computer Science, pages 59-103, 2005. DOI BIB
  • Lijun Zhang, Holger Hermanns (), David N. Jansen: Logic and Model Checking for Hidden Markov Models. In Formal Techniques for Networked and Distributed Systems - FORTE 2005, 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005, Proceedings, volume 3731 of Lecture Notes in Computer Science, pages 98-112, 2005. DOI BIB