研究领域主要是基于马尔科夫模型及其扩展的概率并发系统的模型检验。作为模型检验的重要扩展，概率模型检验是热门前沿基础研究领域之一。学术成果在著名会议和杂志上发表，例如 CAV、CONCUR、LICS、POPL、ETAPS／TACAS、LMCS、 AAAI、Inf. & Comp.等。论文请参考：
http://iscasmc.ios.ac.cn/?page_id=819

   

081202-计算机软件与理论

模型检测，形式化方法
深度学习模型应用
自动驾驶仿真系统

2000-10--2008-12   德国萨尔大学   本科，研究生，博士

   

2012-11~2013-05,丹麦科技大学, 副教授
2010-04~2012-10,丹麦科技大学, 助理教授
2009-12~2010-03,牛津大学, 助理研究员（Research Assistant）
2008-12~2009-11,德国萨尔大学, 博士后

2013-12-31-2014-07-01,利物浦大学访问教授,
2012-10-31-2013-09-30,德国萨尔大学客座教授,

离散数学
强化学习
15级本科毕业论文指导
理论计算机科学基础
用随机模型验证技术的高级故障树分析

   

（1） 中国科学院大学领雁奖, , 院级, 2023
（2） 2022年度中国科学院优秀导师, 院级, 2022
（3） Recognition of Service Award, 一等奖, 其他, 2020
（4） 中国科学院****终期评估优秀, 一等奖, 院级, 2018

   

[1] Weizhi Feng, Yong Li, Andrea Turrini, Moshe Vardi, Lijun Zhang. On the Power of Finite Ambiguity in B\"uchi Complementation. Infomation and Computation[J]. 2023, 第 5 作者  通讯作者  292(105032): 
[2] 任德金, 卢万里, 吕继东, 张立军, 薛白. Model Predictive Control with Reach-Avoid Analysis. International Joint Conference on Artificial Intelligence (IJCAI 2023). 2023, 第 4 作者
[3] Liang Zhang, Nathaniel Xu, Pengfei Yang, Gaojie Jie, Chengchao Huang, Lijun Zhang. TRAJPAC: Towards Robustness Verification of Pedestrian Trajectory Prediction Models. 2019 IEEE/CVF International Conference on Computer Vision (ICCV). 2023, 第 6 作者  通讯作者  
[4] Vojnar, Tomas, Zhang, Lijun. Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2019. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. 2022, 第 2 作者24(1): 29-31, http://dx.doi.org/10.1007/s10009-021-00642-y.
[5] 于世禛, 董一凡, 刘玖阳, 李勇, 吴志林, David N. Jansen, 张立军. Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). SEFM 2022. 2022, 第 7 作者
[6] Li, Renjue, Yang, Pengfei, Huang, ChengChao, Sun, Youcheng, Xue, Bai, Zhang, Lijun. Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning. 2022, 第 6 作者
[7] 李勇, Andrea Turrini, 冯维直, Moshe Vardi, 张立军. Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. 2022, 第 5 作者  通讯作者  
[8] Pengfei Yang, Renjue Li, Jianlin Li, ChengChao Huang, Jingyi Wang, Jun Sun, Bai Xue, Lijun Zhang. Improving Neural Network Verification through Spurious Region Guided Refinement. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS[J]. 2021, 第 8 作者  通讯作者  12651: 389-408, https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979199/.
[9] 张立军. A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. CAV. 2016, 第 1 作者  通讯作者  
[10] Fearnley, John, Rabe, Markus N, Schewe, Sven, Zhang, Lijun. Efficient approximation of optimal control for continuous-time Markov games. INFORMATION AND COMPUTATION[J]. 2016, 第 4 作者  通讯作者  247: 106-129, http://dx.doi.org/10.1016/j.ic.2015.12.002.
[11] Zhang, Lijun, Jansen, David N. A space-efficient simulation algorithm on probabilistic automata. INFORMATION AND COMPUTATION[J]. 2016, 第 1 作者  通讯作者  249: 138-159, http://dx.doi.org/10.1016/j.ic.2016.04.002.
[12] He, Fei, Gao, Xiaowei, Wang, BowYaw, Zhang, Lijun. Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems. ACM SIGPLAN NOTICES[J]. 2015, 第 4 作者50(1): 503-514, http://dx.doi.org/10.1145/2775051.2676998.
[13] Li Meilun, She Zhikun, Turrini Andrea, Zhang Lijun, AAAI. Preference Planning for Markov Decision Processes. PROCEEDINGS OF THE TWENTY-NINTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE. 2015, 第 4 作者3313-3319, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000485625503050.
[14] Chen YuFang, Hong ChihDuo, Wang BowYaw, Zhang Lijun, Kroening D, Pasareanu CS. Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. COMPUTER AIDED VERIFICATION, PT I. 2015, 第 4 作者9206: 658-674, 
[15] 张立军. Probably Safe or Life. CSL-LICS. 2014, 第 1 作者  通讯作者  
[16] Feng, Yuan, Zhang, Lijun, Jones, C, Pihlajasaari, P, Sun, J. When Equivalence and Bisimulation Join Forces in Probabilistic Automata. FM 2014: FORMAL METHODS. 2014, 第 11 作者8442: 247-262, 
[17] Hahn Ernst Moritz, Li Yi, Schewe Sven, Turrini Andrea, Zhang Lijun. IscasMc: A web-based probabilistic model checker. 19th International Symposium on Formal Methods, FM 2014. 2014, 第 5 作者312-317, http://ir.iscas.ac.cn/handle/311060/16510.
[18] Gao, Yang, Xu, Ming, Zhan, Naijun, Zhang, Lijun. Model checking conditional CSL for continuous-time Markov chains. INFORMATION PROCESSING LETTERS[J]. 2013, 第 4 作者  通讯作者  113(1-2): 44-50, https://www.webofscience.com/wos/woscc/full-record/WOS:000312175200009.
[19] Feng, Yuan, Zhang, Lijun. A tighter bound for the self-stabilization time in Herman's algorithm. INFORMATION PROCESSING LETTERS[J]. 2013, 第 2 作者  通讯作者  113(13): 486-488, http://dx.doi.org/10.1016/j.ipl.2013.04.006.
[20] Eisentraut, Christian, Hermanns, Holger, Schuster, Johann, Turrini, Andrea, Zhang, Lijun, Piterman, N, Smolka, SA. The Quest for Minimal Quotients for Probabilistic Automata. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013. 2013, 第 5 作者7795: 16-31, 
[21] Song, Lei, Zhang, Lijun, Godskesen, Jens Chr, Nielson, Flemming. BISIMULATIONS MEET PCTL EQUIVALENCES FOR PROBABILISTIC AUTOMATA. LOGICAL METHODS IN COMPUTER SCIENCE[J]. 2013, 第 2 作者  通讯作者  9(2): https://www.webofscience.com/wos/woscc/full-record/WOS:000322537700002.
[22] Li Jianwen, Zhang Lijun, Pu Geguang, Vardi Moshe Y, He Jifeng, IEEE. LTL Satisfiability Checking Revisited. 2013 20TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING (TIME). 2013, 第 2 作者91-98, 
[23] Zhang, Lijun, Jansen, David N, Nielson, Flemming, Hermanns, Holger. EFFICIENT CSL MODEL CHECKING USING STRATIFICATION. LOGICAL METHODS IN COMPUTER SCIENCE[J]. 2012, 第 1 作者  通讯作者  8(2): https://doaj.org/article/5c7885929a2a40b5ab101174893d7c37.
[24] Eisentraut, Christian, Hermanns, Holger, Zhang, Lijun, IEEE. On Probabilistic Automata in Continuous Time. 25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010). 2010, 第 3 作者342-351, 
[25] Hahn, Ernst Moritz, Li, Guangyuan, Schewe, Sven, Turrini, Andrea, Zhang, Lijun. Lazy Probabilistic Model Checking without Determinisation. 第 5 作者http://arxiv.org/abs/1311.2928.
[26] Yang, Pengfei, Jansen, David N., Zhang, Lijun. Distribution-based bisimulation for labelled Markov processes. 第 3 作者http://arxiv.org/abs/1706.10049.

（1） 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, LIPICS, 2018-09, 第 2 作者
（2） SETSS: Learning Büchi Automata and Its Applications, LNCS, 2019-04, 第 4 作者
（3） 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, LNCS, 2019-04, 第 2 作者

https://iscasmc.ios.ac.cn/?page_id=148