西安电子科技大学计算机科学与技术学院导师教师师资介绍简介-田聪

删除或更新信息，请邮件至freekaoyan#163.com(#换成@)

本站小编 Free考研考试/2021-06-27

田聪(Cong Tian)
教授，博士生导师
西安电子科技大学计算机学院，西安，中国
西安电子科技大学北校区
电子邮箱: ctian at mail.xidian.edu.cn or tico_tools@163.com

简历
西安电子科技大学计算机学院教授，博士生导师。分别于2004年，2007年和2009年在西安电子科技大学获学士、硕士和博士学位。于2010年10月1日至2011年3月31日在日本Hosei大学访问。2013年获国家自然科学基金优秀青年基金和教育部新世纪优秀人才计划资助。2014年获陕西省青年科技新星称号。

研究兴趣
软件安全：程序漏洞分析，恶意代码检测
基于大数据和机器学习的智能软件开发方法
嵌入式软件
可信软件的基础理论与方法

发表的论文
论文列表
DBLP主页链接

教学
形式语言与自动机（硕士研究生，2011春）
Java 程序设计（本科三年级，2011秋）
编译原理（本科三年级，2012春，2013春，2014春，2015春）
验证技术（博士研究生，2012春）
程序语义与形式化验证（硕士、博士研究生，2015春）

科研项目
国家自然科学基金优秀青年基金：形式化验证（NSFC **，2014.01-2016.12）
国家自然科学基金面上项目：基于共享变量的多核并发程序模型检测（NSFC **，2013.01-2016.12）
国家自然科学基金青年基金项目：基于APTL的开放系统模型检测（NSFC **，2011.01-2013.12）
国家自然科学基金重点国际合作项目（合作方：英国牛津大学和美国UTD）：基于语义的恶意程序主动防御与检测机理研究（NSFC ，2015.01-2019.12）
国家自然科学基金可信软件重大专项重点项目：C/Verilog程序的MSVL验证理论与方法（NSFC **，2015.01-2016.12）
国家自然科学基金重点项目：开放软件系统的基础理论与关键技术（NSFC **, 2012.01-2016.12 ）
*科研项目*973子课题：信息服务的需求获取与建模
国家自然科学基金重大国际合作项目(英、法、日)，构造可信、高效软件系统的基础研究
国家自然科学基金可信软件重大专项培育项目：基于FPGA的高可信嵌入式系统的基础研究

奖励及资助
国家自然科学基金优秀青年基金资助（2013）
教育部自然科学一等奖
教育部新世纪优秀人才资助（2013）
陕西省青年科技新星（2014）
陕西省中青年科技领军人才（2014）
西安电子科技大学第二届优秀青年教师资助计划
陕西省科学技术一等奖
西安电子科技大学优秀博士论文
西安电子科技大学优秀博士论文资助计划

招生说明
每年招生硕士研究生7名，博士研究生1-2名。欢迎大家保送或者报考。
每年招收1-2名优秀本科在读生（2年级以上）进入课题组，欢迎优秀学子加盟。

研究兴趣
软件安全：程序漏洞分析，恶意代码检测
基于大数据和机器学习的智能软件开发方法
嵌入式软件
可信软件的基础理论与方法

发表的论文
论文列表
DBLP主页链接

Cong Tian(田聪)
Professor
School of Computer Science and Technology
Xidian University, Xi'an, China
Emails: ctian at mail.xidian.edu.cn or tico_tools@163.com

News
[Apr 5, 2016] Our paper "Decision Procedure for A Fragment of Linear Time Mu-Calculus" was accepted by IJCAI 2016.
[Jan 13, 2016] Our paper "Model Checking Petri Nets with MSVL" was accepted at Information Sciences.
[Dec 1, 2015] Our group earned Natural Science Award (first class) from the Ministry of Education.
Biography
Cong Tian received Ph.D., M.Sc. and B.Sc. in Computer Science fromXidian University, China, in 2009, 2007 and 2004, respectively. She is now a professorat the school of computer science and technology, Xidian University, Xi'an, China. From 1st Oct 2010 to 31st March 2011,shewas a HIF researcher at theSoftware Engineering Laboratory for Dependable Systems,Hosei University, Tokyo, Japan.Research Interests
Cong's research interestsarein formal verification, both the theoretical and practical aspects.Theseinclude:Theories in model checking, temporal logics and automata
Formal verification of software systems
Logic programming
Publications
Publications
DBLP Entry
Teaching
Formal Language and Automata Theory (2011)
Java Programming (2011)
Compilers (2012, 2013,2014)
Formal Verification (2012)
Academic Services
Editor ofjournal of combinatorial optimization
Editor of journal of software
SOFL+MSVL 2016 PC Co-chair
SNPD 2016 PC Member
SETTA 2016 PC Member
ESSS 2015 PC Member
SOFL+MSVL 2015 PC Member
ICECCS 2014PC Member
EASLLC 2014PC Member
SOFL+MSVL 2014 PC Member
SOFL+MSVL 2013 PC Member
WSOFL 2012 PC Member
TASE2011 PC Member
Useful Links
CC Source Code
n-full ordered tree with canonical flags generator
GCEGAR(Change the extension to be .jar for excuting with JVM)
Data

Back to Home
2016
Journal papers:
Ya shi,Cong Tian*, Zhenhua Duan*.Model Checking Petri Nets with MSVL. Information Sciences, Vol 363: 274-291. DOI:10.1016/j.ins.2016.01.036
Zhenhua Duan, Cong Tian*, Mengchu Zhou, Xiaobing Wang, Nan Zhang, Hongwei Du, Lei Wang. Two-la[ant]yer hybrid peer-to-peer networks. Peer-to-Peer Networking and Applications.DOI: 10.1007/s12083-016-0460-5.
Nan Zhang, Zhenhua Duan*, Cong Tian*. A Mechanism of Function Calls in MSVL，Theoretical Computer Science,doi:10.1016/j.tcs.2016.02.037.
Conference papers:
Yao Liu,Zhenhua Duan*, Cong Tian*. A Decision Procedure for A Fragment of Linear-Time Mu-Calculus. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI 2016)，1195 - 1201.
2015
Journal papers:
Zhenhua Duan, Cong Tian*, and Nan Zhang.A Canonical Form Based Decision Procedure and Model Checking Approach for Propositional Projection Temporal Logic. Theoretical Computer Science, 609: 544-560, 2016. doi:10.1016/j.tcs.2015.08.039.
Zhenhua Duan, Jin Liu, Jie Li, Cong Tian*.Improved Even Order Magic Square Construction Algorithms and Their Applications in Multi-user Shared Electronic Accounts. Theoretical Computer Science, 607: 391-410. 10.1016/j.tcs.2015.07.053.
Nan Zhang, Zhenhua Duan, and Cong Tian. A Complete Axiomation for Propositional Projection Temporal Logic with cylinder computation model. Theorectical Computer Science. DOI:10.1016/J.TCS.2015.05.007,2015.
Jin Liu, Zhenhua Duan, Cong Tian, and Nan Zhang.An extended strange planet protocol. Journal of Combinatorial Optimization, Volume 30, Issue 2, pp 299-319, Aug 2015.
Ling Luo, Zhenhua Duan,Cong Tian, and Xiaobing Wang.A structural transformation from p-π to MSVL. Journal of Combinatorial Optimization, Volume 29, Issue 1 pp 308-329, Jan 2015.
Cong Tianand Zhenhua Duan.Transformation from PLTL to Automata via NFGs. Journal of Combinatorial Optimization, 29 (2), 406-417, 2015.
Conference papers:
Jin Cui, Zhenhua Duan,Cong Tian, and Nan Zhang.Model Checking of a muC/OS-III Multi-task System with TMSVL. The 17th International Conference on Formal Engineering Methods(ICFEM 2015), Springer-Verlag, LNCS 9407, 187-200, 2015.
Zhenhua Duan, Kangkang Bu,Cong Tian, Nan Zhang. Model Checking MSVL Programs Based on Dynamic Symbolic Execution.In proceedings of the 21th Annual International Computing and Combinatorics Conference (COCOON 2015), Springer-Verlag, LNCS 9198, pp 521-533, 2015.
2014
Journal papers:
Kai Yang, Zhenhua Duan, and Cong Tian.Modeling and Verification of RBC Handover Protocol. Electronic Notes in Theoretical Computer Science,Volume 309, Pages 51–62,22 December 2014.
Bin Yu, Zhenhua Duan, andCong Tian.Bounded Model Checking of Traffic Light Control System. Electronic Notes in Theoretical Computer Science,Volume 309, Pages 63–74,22 December 2014.
Cong Tian, Zhenhua Duan, and Zhao Duan. Making CEGAR More Efficient in Software Model Checking. IEEE Transactions on Software Engineering (TSE), Vol 40(12), 1206-1223, Dec 2014. DOI:10.1109/TSE.2014.**, 2014.
Zhenhua Duan and Cong Tian. A Practical Decision Procedure for Propositional Projection Temporal Logic with Infinite Models. Theorectical Computer Science.Vol 554, pp. 169-190, 2014.Doi:10.1016/j.tcs.2014.02.011
Nan Zhang, Zhenhua Duan, Cong Tian, and Dingzhu Du. AformalproofofthedeadlinedrivenschedulerinPPTLaxiomaticsystem.Theoretical Computer Science.Vol 554, pp. 229-253, 2014.Doi:10.1016/j.tcs.2013.12.014
Cong Tian, Shaoying Liu, and Zhenhua Duan.Test Case Generation from Conjunctions of Predicates with Model Checking. Chinese Journal of Electronics, Vol 23, No 2, 271-277, 2014.
Cong Tian, Zhenhua Duan, and Jin Liu.Secure Communications with Strange Planet Protocol.Optimization Letters, 8(1), 201-209, 2014. DOI:10.1007/s11590-012-0561-x.
Conference papers:
Zhenhua Duan andCong Tian.Normal Form ex[ant]pressions for Propositional Projection Temporal Logic. In proceedings of the 20th Annual International Computing and Combinatorics Conference (COCOON 2014), LNCS 8591, pp 84-93,Atlanta, Georgia, USA, 2014.
Nan Zhang, Zhenhua Duan andCong Tian.An Axiomatization for Cylinder Computation Model. In proceedings of the 20th Annual International Computing and Combinatorics Conference (COCOON 2014), LNCS 8591, pp 71-83,Atlanta, Georgia, USA, 2014.
Bo Zhou, Xin Xia, David Lo,Cong Tian, and Xinyu Wang.Towards More Accurate Content Categorization of API Discussions. In proceedings of the 22thInternational Conference on Program Comprehension (ICPC 2014), PP. 95-105,Hyderabad, India, 2014.
Yao Liu, Zhenhua Duan, and Cong Tian. An Improved Recursive Algorithm for Parity Games.The 8th International Symposium on Theoretical Aspects of Software Engineering(TASE 2014), pp 154-161, 2014.
Jin Cui, Zhenhua Duan, and Cong Tian. Model Checking Rate-Monotonic Scheduler with TMSVL. The 19th International Conference on Engineering of Complex ComputerSystems(ICECCS 2014), pp 202-205, 2014.
Kai Yang, Zhenhua Duan,Cong Tian. A Memory Management Mechanism for MSVL. SOFL+MSVL 2014: 179-188
Bin Yu, Zhenhua Duan,Cong Tian. Unified Bounded Model Checking for MSVL. SOFL+MSVL 2014: 49-61
Quanrun Fan, Zhenhua Duan, Cong Tian, Hongwei Du. Clustering and Partition Based Divide and Conquer for SAT Solving. MSN 2014: 299-307
Nan Zhang, Zhenhua Duan, Cong Tian. Extending MSVL with Function Calls.the 17th International Conference on Formal Engineering Methods(ICFEM 2015),446-458.
Meng Wang, Zhenhua Duan, Cong Tian.Simulation and verification of the virtual memory management system with MSVL. CSCWD 2014: 360-365
Zhenhua Duan, Jin Liu, Jie Li, Cong Tian. Improved Even Order Magic Square Construction Algorithms and Their Applications. COCOA 2014: 666-680
2013
Journal papers:
Nan Zhang, Zhenhua Duan, andCong Tian.Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic. Chinese Journal of Electronics, Vol 22, Issue (CJE-1): 21-24, 2013.
Conference papers:
Jin Liu, Zhenhua Duan, andCong Tian.An Extended Strange Planet Protocol. In proceedings of the 7th Annual International Conference on Combinatorial Optimization and Applications(COCOA 2013), LNCS 8287, Springer-Verlag, pp 214-225.
Ya Shi, Zhenhua Duan, andCong Tian.Translation from Workflow Nets to MSVL. In Proceedings of the 15th International Conference on Formal Engineering Methods (ICFEM 2013), LNCS 8144,Springer-Verlag,pp 281-296, 2013.
Xu Lu, Zhenhua Duan,Cong Tian, and Hongjin Liu.Integrating Separation Logic with PPTL. SOFL+MSVL 2013, 35-47.
Ya Shi, Zhenhua Duan,Cong Tian, and Hua Yang.Improving Net Reductions for LTLX Model Checking. SOFL+MSVL 2013, 48-61.
Yao Liu, Zhenhua Duan,Cong Tian, and Bo Liu. Present-Future Form of Linear Time Mu-Calculus. SOFL+MSVL 2013, 76-85.
Peng Zhang, Zhenhua Duan, andCong Tian.Simulation of CTCS-3 Protocol with Temporal Logic Programming. CSCWD 2013, 72-77.
Zhenhua Duan, Qian Ma,Cong Tian, and Nan Zhang.Some Fixed-Point Issues in PPTL. Theories of Programming and Formal Methods 2013,151-165,2013.
Cong Tian, Zhenhua Duan and Mengfei Yang.Deternimization of Büchi Automata as Partitioned Automata. Proceedings of the 19th Annual International Computing and Combinatorics Conference (COCOON 2013), 158-168, 2013.
Zhenhua Duan,Cong Tian, Mengfei Yang and Jia He.Bounded Model Checking for Propositional Projection Temporal Logic.Proceedings of the 19th Annual International Computing and Combinatorics Conference (COCOON 2013), 591-602, 2013.
Cong Tianand Zhenhua Duan.Detecting Spurious Counterexamples Efficiently in Abstract Model Checking. Proceedings of the 35th International Conference on Software Engineering (ICSE 2013), 202-211, 2013.
Cong Tian, Shaoying Liu and Zhenhua Duan.Abstract Model Checking with SOFL Hierachy.Proceedings of WSOFL 2012, LNCS 7787, 71-86, 2013.
Yan Yu, Zhenhua Duan,Cong Tianand Mengfei Yang.Model Checking C Programs with MSVL.Proceedings of WSOFL 2012, LNCS 7787, 87-103, 2013.
Papers in Chinese:
Pengcheng Nie, Zhenhua Duan,Cong Tian, and Mengfei Yang.Adaptive Scheduling on Performance Asymmetric Multicore Processors,Chinese Journal of Computers,2013, 36(4),773-781.
2012
Journal papers:
Cong Tian, Zhenhua Duan. An Efficient Approach forAbstraction Refinement in Model Checking. Theoretical Computer Science, Vol 461, 76-85, 2012. DOI:10.1016/j.tcs.2011.12.014
Nan Zhang, Zhenhua Duan, andCong Tian. A cylinder computation model for many-core parallel computing. Theoretical Computer Science(2012), Vol: 497, 68-83, 2013, doi:10.1016/j.tcs.2012.02.011.
Conference papers:
Cong Tianand Zhenhua Duan.A Practical Transformation from LTL to Automata.CNSI 2012, pp.638-643, 2012.
Tao Pang, Zhenhua Duan,Cong Tian.Symbolic Model Checking for Propositional Projection Temporal Logic. TASE 2012: 9-16.
Chapters:
Zhenhua Duan andCong Tian.Temporal Logic and Model Checking. Handbook of Finite State Based Models and Applications. SBN-10:. Chapman & Hall. Aug 2012.
2011
Journal papers:
Cong Tian and Zhenhua Duan, Expressiveness of Propositional Projection Temporal Logic, Theoretical Computer Science, Volume 412, Issue 18, Aug, 2011, Pages 1729-1744. DOI:10.1016/j.tcs.2010.12.047.
Conference papers:
Sven Schewe andCong Tian.Synthesising Classic and Interval Temporal Logic. In the proceedings ofthe18th International Symposium on Temporal Representation and Reasoning (TIME2011), 64-71, IEEE Computer Society, 2011.
Cong TianandZhenhua Duan.Focus Game for PITL with Infinite Models. In the proceedings of TASE 2011, 45-51, IEEE Computer Society, 2011.
Cong Tianand Zhenhua Duan.Making Abstraction Refinement Efficient in Model Checking. The 17th International Conference COCOON 2011,Springer-verlag LNCS 6842, 90-111, 2011.
Cong Tian, Shaoying Liu and Shin Nakajima.Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Predicates. The proceedings of CSTAV 2011, 304-309, IEEE Conputer Society.
Papers in Chinese:
Cong Tian,Zhenhua Duan.Model Checking Rate Monotonic Scheduling Algorithm based on Propositional Projection Temporal Logic. Journal of Software,2011,22(2):211-221.
Chen Zhang, Zhenhua Duan,Cong Tian.Specification and Verification of UML2.0 Sequence Diagrams based on Event Deterministic Finite Automata. Journal of Software,2011,22(11):2625-2638.
2010
Conference papers:
Cong TianandZhenhua Duan.A Transformation from PPTL to S1S. In the proceedings of COCOA 2010. Part 2, LNCS 6509, 374-386, 2010.
Cong Tianand Zhenhua Duan.Alternating Interval based Temporal Logics. Proceedings of 12th International Conference on Formal EngineeringMethods (ICFEM2010), LNSC 6447, Springer-Verlag,16-19 Nov. 2010, pp. 694-709.
Zhenhua Duan andCong Tian.An Improved Decision Procedure for Propositional Projection Temporal Logic.Proceedings of 12th International Conference on Formal EngineeringMethods (ICFEM2010), LNSC 6447, Springer-Verlag,16-19 Nov. 2010, pp. 90-105.
Xiaoyu Song, Zhenhua Duan, andCong Tian.Non-Functional Requirements Elicitation and Incorporation into Class Diagrams. Intelligent Information Processing 2010: 72-81.
Zhenhua Duan andCong Tian.An Executable Concurrent Model for OWL-S Process Models. QSIC 2010, pp. 405-413, IEEE Conputer Society, July 2010.
2009
Journal papers:
Cong Tian and Zhenhua Duan, A Note on Stutter-Invariant PLTL, Information Processing Letters, 109 (13): 663-667, 2009.
Cong Tian and Zhenhua Duan, Complexity of Propositional Projection Temporal Logic with Star, Mathematical Structures in Computer Science, vol.19, pp.73-100, Cambridge University Press, 2009.
2008
Journal papers:
Zhenhua Duan, Cong Tian, and Li Zhang, A Decision Procedure for Propositional Projection Temporal Logic with Infinite Models. Acta Informatica, 45(1),43-78, Springer-verlag, 2008.
Conference papers:
Zhenhua Duan and Cong Tian, A Unified Model checking Approach with Projection Temporal Logic, ICFEM2008,LNCS5256, pp 167-186, Springer-verlag, Oct, 2008.
Cong Tian and Zhenhua Duan, Propositional Projection Temporal Logic, Buchi Automata and omega-Regular ex[ant]pressions, TAMC 2008, LNCS 4978, pp 47-58, Springer-verlag, April, 2008.
2007
Conference papers:
Cong Tian and Zhenhua Duan, Model Checking Propositional Projection Temporal Logic based on SPIN. ICFEM 2007, LNCS4789 , pp 246-265, Springer-verlag, Nov, 2007.
Zhenhua Duan andCong Tian, Decidability of Propositional Projection Temporal Logic with Infinite Models. TAMC 2007, LNCS4484 , pp 521-532, Springer-verlag, May, 2007.

LTLNFBA
LTLNFBA is a tool that translate an LTL formula to Buchi automata. The tools is developed based on LTL2BA with the tranlating algorihtm changed and new rules for improving the translation.
Download and Installation
Source code of the newest version of LTLNFBA can be downloaded here (ltlnfba(v1).tar.gz NOTE: the suffix to be changed to .tar.gz). To compile the source code, linux + gcc are required.
Introduction
Spin syntax as well as commands used in LTL2BA are all kept in LTLNFBA. So a user who can use LTL2BA can also use LTLNFBA.
Here you can find all the formulas involved in the experiment of LTNNFBA.

TPChecker
TPChecker is a tool for verifying temporal properties of C programs.
Download and Installation:
The tool is available at (1, 2, 3, 4) . The platform is windows OS and Eclipse. First, you need to install a Java Runtime Environment which is at least Java 7 compatible. Second, you need to create a folder D:property, and put the following three files inside it:
properties.txt: to save the property to be checked;
allPointers.txt: to save all the pointers in C programs when checking null pointer dereference. Note that in CTPChecker, we also developed a module to support automic property formalizing for checking null pointer dereference in C programs.
proposition.txt: to save the corresponding predicates.
How to use?
1. Choose a source code file (C program) that you want to check.
2. Choose a configuration file. Standard configuration files can be found in the directory config/. These are two extended configuration files, predicateAnalysis-PredAbsRefiner-SBE-pointer.properties and predicateAnalysis-PredAbsRefiner-SBE-simpleproperty.properties.
3. Write the property to D:propertyproperties.txt and the propisitions to D: propertypropositions.txt.
Note that if you check the null pointer dereference, the property can be created automatically. So, you don’t need to write it to the file D:propertypropositions.txt.
4. Execute the command "sc[ant]ripts/cpa.bat [ -config ] ", e.g. sc[ant]ripts/cpa.bat -config config/predicateAnalysis PredAbsRefiner-SBE-pointer.properties example.c

Brief Intro.
HybVeri is an efficient software model checker for safety property verification of C programs.
Download and Installation:
The tool is avaible at Here (part-1,part-2, part-3, part-4, part-5). The platform is Windows OS and Eclipse. First, you need to install a Java Runtime Envirnment which is at least Java 7 comptble. Second, you need to create a folder F:at and put the following file inside:
exeProgram.bat: the file can compile test-comb.c to generate the test-comb.exe. test-comb.c is a temporal file to run the complex loops. The content ofexeProgram.bat is as follows:
C:
cd C:Program FilesMicrosoft Visual StudioVC98Bin
call VCVARS32.BAT
F:
cd F:bat
cl test-comb.c
The directory C:Program FilesMicrosoft Visual StudioVC98Bin is the location of the file VCVARS32.BAT. You need to replace it with your directory.
How to use?
1. Choose a source code file (C program) that you want to check.
2. Choose a configuration file. Standard configuration files can be found in the directory config. Choose the file predicateAnalysis-PredAbsRefiner-SBE.properties .
3. Execute the command "java -jar HybVeri.jar [ -config ] < SOURCE_FILE>", e.g.java –jar HybVeri.jar -config configpredicateAnalysis-PredAbsRefiner-SBE.properties example.c.
Experiments: Crude Data

Brief Introducation
CEGFixer is a tool supporting automatic memory-leak fixing in C programs. It utilize a software model checker to check memory-leaks in C programs. Then under the guidance of counterexamples produced by the software model checker, the leaks in programs are repaired.

Benchmark
Benmark for CoverageEvaluation