基本信息
张立军  男  博导  中国科学院软件研究所
电子邮件: zhanglj@ios.ac.cn
通信地址: 北京市海淀区中关村南四街4号
邮政编码:

研究领域

研究领域主要是基于马尔科夫模型及其扩展的概率并发系统的模型检验。作为模型检验的重要扩展,概率模型检验是热门前沿基础研究领域之一。学术成果在著名会议和杂志上发表,例如 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,德国萨尔大学, 博士后
2000-10~2008-12,德国萨尔大学, 本科,研究生,博士
社会兼职
2013-12-31-2014-07-01,利物浦大学访问教授,
2012-10-31-2013-09-30,德国萨尔大学客座教授,

教授课程

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

专利与奖励

   
奖励信息
(1) Recognition of Service Award, 一等奖, 其他, 2020
(2) 中国科学院****终期评估优秀, 一等奖, 院级, 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, 292(105032): [2] 任德金, 卢万里, 吕继东, 张立军, 薛白. Model Predictive Control with Reach-Avoid Analysis. International Joint Conference on Artificial Intelligence (IJCAI 2023)null. 2023, [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)null. 2023, [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, 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 2022null. 2022, [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, [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 IInull. 2022, [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, 12651: 389-408, https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979199/.
[9] 张立军. A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. CAV. 2016, [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, 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, 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, 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 INTELLIGENCEnull. 2015, 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 Inull. 2015, 9206: 658-674, [15] 张立军. Probably Safe or Life. CSL-LICS. 2014, [16] Feng, Yuan, Zhang, Lijun, Jones, C, Pihlajasaari, P, Sun, J. When Equivalence and Bisimulation Join Forces in Probabilistic Automata. FM 2014: FORMAL METHODSnull. 2014, 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 2014null. 2014, 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, 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, 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 2013null. 2013, 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, 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)null. 2013, 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, 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)null. 2010, 342-351, [25] Hahn, Ernst Moritz, Li, Guangyuan, Schewe, Sven, Turrini, Andrea, Zhang, Lijun. Lazy Probabilistic Model Checking without Determinisation. http://arxiv.org/abs/1311.2928.
[26] Yang, Pengfei, Jansen, David N., Zhang, Lijun. Distribution-based bisimulation for labelled Markov processes. 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