基本信息
张立军  男  博导  中国科学院软件研究所
电子邮件: 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] 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/.
[2] Li, Yong, Chen, YuFang, Zhang, Lijun, Liu, Depeng. A novel learning algorithm for Buchi automata based on family of DFAs and classification trees. INFORMATION AND COMPUTATION[J]. 2021, 281: http://dx.doi.org/10.1016/j.ic.2020.104678.
[3] Li, Jianwen, Zhu, Shufang, Pu, Geguang, Zhang, Lijun, Vardi, Moshe Y. SAT-based explicit LTL reasoning and its application to satisfiability checking. FORMAL METHODS IN SYSTEM DESIGN[J]. 2019, 54(2): 164-190, https://www.webofscience.com/wos/woscc/full-record/WOS:000494821000002.
[4] Chen YuFang, Heizmann Matthias, Lengal Ondrej, Li Yong, Tsai MingHsien, Turrini Andrea, Zhang Lijun, Foster JS, Grossman D. Advanced Automata-Based Algorithms for Program Termination Checking. PLDI'18: PROCEEDINGS OF THE 39TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATIONnull. 2018, 135-150, http://dx.doi.org/10.1145/3192366.3192405.
[5] Li, Yongjian, Duan, Kaiqiang, Jansen, David N, Pang, Jun, Zhang, Lijun, Lv, Yi, Cai, Shaowei. An Automatic Proving Approach to Parameterized Verification. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC[J]. 2018, 19(4): https://www.webofscience.com/wos/woscc/full-record/WOS:000452804000004.
[6] Eisentraut, Christian, Hermanns, Holger, Schuster, Johann, Turrini, Andrea, Zhang, Lijun. The quest for minimal quotients for probabilistic and Markov automata. INFORMATION AND COMPUTATION[J]. 2018, 262(Pt.1): 162-186, http://dx.doi.org/10.1016/j.ic.2018.08.003.
[7] Zhang, Lijun, Yang, Pengfei, Song, Lei, Hermanns, Holger, Eisentraut, Christian, Jansen, David N, Godskesen, Jens Chr. Probabilistic bisimulation for realistic schedulers. ACTA INFORMATICA[J]. 2018, 55(6): 461-488, https://www.webofscience.com/wos/woscc/full-record/WOS:000440646900002.
[8] Feng, Yuan, Zhang, Lijun. Precisely deciding CSL formulas through approximate model checking for CTMCs. JOURNAL OF COMPUTER AND SYSTEM SCIENCES[J]. 2017, 89: 361-371, https://www.webofscience.com/wos/woscc/full-record/WOS:000408293400021.
[9] 张立军. On Equivalence Checking of Nondeterministic Finite Automata. SETTA. 2017, [10] Feng, Yijun, Zhang, Lijun, Jansen, David N, Zhan, Naijun, Xia, Bican, DSouza, D, Kumar, KN. Finding Polynomial Loop Invariants for Probabilistic Programs. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2017)null. 2017, 10482: 400-416, [11] 张立军. A 77GHz Power Amplifier Design Scheme for Automotive Radar. 2017 International Conference on Electron Devices and Solid-State Circuits (EDSSC). 2017, [12] 张立军. Common-Mode-Switched Inductor for Low Phase Noise and Wide Frequency Tuning Range. IEEE Transactions on Circuits and Systems I: Regular Papers. 2017, [13] Chen, Xianhong, Zhang, Lijun, Xu, Can, Liu, Hui, Zheng, Zhanqi. Coupling matrix synthesis for dual-band bandpass filters based on admittance poles and zeros. MICROWAVE AND OPTICAL TECHNOLOGY LETTERS[J]. 2016, 58(3): 603-606, https://www.webofscience.com/wos/woscc/full-record/WOS:000369166100027.
[14] 张立军. A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. CAV. 2016, [15] 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.
[16] 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.
[17] 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, https://www.webofscience.com/wos/woscc/full-record/WOS:000354800500041.
[18] 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, [19] 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.
[20] Peng, Yatao, Zhang, Lijun, Fu, Jun, Wang, Yudong, Leng, Yongqing. Modified output impedance matching solution for load modulation power amplifier performance enhancing. IET MICROWAVES ANTENNAS & PROPAGATION[J]. 2015, 9(13): 1376-1385, http://www.irgrid.ac.cn/handle/1471x/1091961.
[21] Chen, Xianhong, Zhang, Lijun, Peng, Yatao, Leng, Yongqing, Lu, Hui, Zheng, Zhanqi. COMPACT LOWPASS FILTER WITH WIDE STOPBAND BANDWIDTH. MICROWAVE AND OPTICAL TECHNOLOGY LETTERS[J]. 2015, 57(2): 367-371, https://www.webofscience.com/wos/woscc/full-record/WOS:000346595600024.
[22] Peng Yatao, Zhang Lijun. A 400MHz to 4GHz image-reject up convert mixer integrated a broadband quadrature signal generator. 2015, http://www.irgrid.ac.cn/handle/1471x/1091965.
[23] 张立军. Probably Safe or Life. CSL-LICS. 2014, [24] 张立军. A Dual-mode Dual-band Bandpass Filter Using Tri-stubs Loaded Multimode Resonaor. Journal of Electromagnetic Waves and Applications. 2014, [25] Chen Xianhong, Zhang Lijun, Peng Yatao. Novel UWB Bandpass Filter with Sharp Rejection and Narrow Notched Band. ELECTRONICS LETTERS[J]. 2014, http://www.irgrid.ac.cn/handle/1471x/1092967.
[26] 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, [27] 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.
[28] 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.
[29] 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, https://www.webofscience.com/wos/woscc/full-record/WOS:000319493400006.
[30] 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, [31] 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.
[32] 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, [33] Koutsoukos, Xenofon. "Safety Verification for Probabilistic Hybrid Systems". EUROPEAN JOURNAL OF CONTROL[J]. 2012, 18(6): 588-590, http://dx.doi.org/10.3166/EJC.18.572-587.
[34] 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://www.webofscience.com/wos/woscc/full-record/WOS:000307646300017.
[35] 张立军. Automata-based CSL model checking. International Colloquium on Automata, Languages and Programming (ICALP). 2011, [36] 张立军. Model Checking Algorithms for CTMDPs. Computer Aided Verification (CAV). 2011, [37] 张立军. A Real-Time and High-Precision Algorithm for Frequency Estimation by Fusing Multisection Signals. CEIS International Conference on Advanced. 2011, [38] 张立军. Experiments with Phase-delay Method for Slow Light in Photonic Crystal Waveguide. International Conference on Electric Information and Control Engineering. 2011, [39] Sun, Z Y, Zhang, L J, Yan, Y P, Yang, H W. UNEQUAL DUAL-BAND RAT-RACE COUPLER BASED ON DUAL-FREQUENCY 180 DEGREE PHASE SHIFTER. JOURNAL OF ELECTROMAGNETIC WAVES AND APPLICATIONS[J]. 2011, 25(13): 1840-1850, http://10.10.10.126/handle/311049/9125.
[40] 孙征宇. A Novel Unequal Dual-band Gysel Power Divider. 2011 IEEE MTT-S International Microwave Symposium Digest (MTT)null. 2011, http://10.10.10.126/handle/311049/9471.
[41] 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, [42] 张立军. 基于光纤的矢量和微波光子移相器方案设计. 《空军工程大学学报》. 2010, [43] 张立军. 微纳光子晶体波导慢光结构制作与实验研究. 第三届微纳电子技术交流与学术研讨会. 2010, [44] 张立军. 14. Design of CAN Bus Embedded System Applied to New-Type Solid-state Transmitting System. 2006, [45] 张立军. A New Generation of S-Band Solid State 16KW Transmitter for ATC Primary Radar. IEEE 1999 International Radar conference. 1999, [46] Yong Li, YuFang Chen, Lijun Zhang, Depeng Liu. A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. Information and Computation. http://dx.doi.org/10.1016/j.ic.2020.104678.
[47] Hahn, Ernst Moritz, Li, Guangyuan, Schewe, Sven, Turrini, Andrea, Zhang, Lijun. Lazy Probabilistic Model Checking without Determinisation. http://arxiv.org/abs/1311.2928.
[48] 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