田聪，教授，博士生导师。于2004年、2007年和2009年在西安电子科技大学先后获学士、硕士和博士学位。主要研究领域：可信软件理论与方法。

自2004年以来，一直从事形式化验证理论和方法领域的研究工作，建立了基于命题投影时序逻辑（Propositional Projection Temporal Logic，PPTL）的模型检测理论与方法。首先，证明了命题区间时序逻辑（Propositional Interval Temporal Logic，PITL）在无穷模型上的可判定性，解决了该逻辑25年悬而未决的判定问题，证明了PPTL的复杂性和表达性，建立了PPTL理论基础。在此基础上，给出了基于SPIN的PPTL模型检测和基于MSVL的统一模型检测算法，并开发了相应的模型检测工具。为了支持投影时序逻辑对开放系统的验证，将PPTL扩展到并发博弈结构，提出了交互式投影时序逻辑（Alternating Projection Temporal Logic，APTL），并给出了相应的判定过程和模型检测算法。为了缓解模型检测中的状态空间爆炸问题，在偏序模型检测方面，给出了当前最好的打结不变（Stutter-invariant）线性时序逻辑产生算法。在抽象模型检测方面，给出了多项式抽象模型精化算法，不仅避免了现有抽象精化过程中的NP完全问题，还可以得到更小的抽象模型。给出了高效的真假反例路径评判算法，对于无穷反例虚假路径检测，原有SPLITPATH方法的时间复杂度是多项式，新提出的检测算法是线性的；对于有穷反例路径，新的虚假路径探测算法可并行化，且可以找出所有导致虚假路径的坏节点。另外，提出了Pop 逻辑（Pop Logic，PL），该逻辑的一个子集的表达能力位于线性时序逻辑（LTL）和PPTL之间，但是其复杂度与LTL相同。

近5年来，主持国家自然科学基金青年基金项目1项（20万），国家自然科学基金面上项目1项（80万）。获2013年国家自然科学基金优秀青年基金资助（100万），2013年教育部新世纪优秀人才计划资助（50万）。曾参加国家自然科学基金重点项目2项，国家自然科学基金重大国际合作项目1项，国家科技发展（973）计划1项。近年来，在相关领域重要国际期刊（Theoretical Computer Science，Mathematical Structures in Computer Science，Acta Informatica等）和重要国际会议（ICSE，ICFEM，COCOON等）发表论文40余篇。