ICSE 2291 ASE 2141 FSE 1566 ASPLOS 1219 LMCS 1020 OOPSLA 737 LICS 679 ISSTA 617 POPL 609 ICFP 374 PLDI 369 TOPLAS 199 JFP 172 arXiv 预印本 5
标签：逻辑与自动机（共 1126 篇，按优先级展示前 200）
连接自然语言与形式规约——使用LLM通过层次语义分解自动将软件需求翻译为LTL
提出Req2LTL，用LLM分层语义分解与规则合成将自然语言需求自动翻译为LTL。
自动化需求形式化：使用 LLM 与低复杂度区分迹进行语义验证
提出 ARTEMIS，用 LLM 将自然语言需求经结构化中间表示译为时序逻辑，并用低复杂度区分迹把人工验证开销对数级削减。
递归状态机引导的上下文无关语言可达性图折叠
提出由递归状态机引导的图折叠算法 GF，通过缩减输入图规模加速 CFL-reachability 程序分析。
论双向交错 Dyck 可达性的复杂度
证明了双向交错 Dyck 可达性的首个可判定变体 D1⊙D1 属于 PTIME，并证明 k≥2 时为 NP-hard，且其过近似更精确。
基于动态双向 Dyck 可达性的即时静态分析
提出每次更新 O(n·α(n)) 的动态双向 Dyck 可达性算法，用于即时静态分析并实现千倍加速。
基于图表示学习的可SAT验证的LTL可满足性检查
提出融合语法与语义的LTL图表示OSUG，用图学习判定可满足性并生成可验证的可满足迹。
使用同步下推系统的上下文、流与字段敏感数据流分析
提出同步下推系统（SPDS），将过程调用/返回与字段读写编码为两个同步的 CFL 可达性问题，实现高精度且可扩展的上下文、流、字段敏感数据流分析。
正几乎必然终止：复杂度与证明规则
证明概率程序的PAST复杂度为Π^1_1完全，并给出基于超限序数的可靠完备证明规则。
通过端到端学习检查LTL可满足性
用端到端神经网络在多项式时间内预测LTL可满足性，并通过保持LTL逻辑性质提升归纳偏置。
强不变式很难：论（概率）程序最强多项式不变式的困难性
证明单路径多项式循环的最强多项式不变式计算至少与 Skolem 问题同难，并推广到概率程序的矩不变式。
CFL 可达性问题的细粒度复杂度
在细粒度复杂度框架下确定 CFL 可达性的精确指数，并证明 Dyck-2 的 Ω(n^2.5) 下界。
AdaRule：基于模式自适应规则归纳的 LLM 驱动自然语言到 LTL 转换
提出 AdaRule，用 LLM 反馈迭代归纳模式自适应翻译规则，免手工规则实现 NL→LTL 转换，平均提升至少 21.1%。
正则语言 Parikh 像的约束求解方法
将正则语言 Parikh 像推理转化为约束求解问题，提出 PC* 演算与工具 Catra，避免显式构造积自动机并显著加速字符串约束求解。
不可判定问题的可见证性
提出“可见证性”概念，证明多数不可判定问题可计算地从任意可判定近似构造出反例输入。
匹配逻辑
提出匹配逻辑，一种以模式与模式匹配统一刻画结构和推理的一阶逻辑变体，可泛化多种程序分析逻辑并支持 SMT 求解。
非确定性自动机的高效约简及其在语言包含测试中的应用
提出高效的 NFA/NBA 约简算法，并显著扩展语言包含等 PSPACE 完全问题的可解规模。
判定具有有限输入和输出的程序的差分隐私
针对有限输入输出程序，研究差分隐私判定的可判定性，填补逻辑与统计方法回避的基础问题。
基于时序不变量的模块化控制平面验证
提出 Timepiece，用逻辑时间路由模型与受时序逻辑启发的接口谓词，实现可靠可扩展的模块化控制平面验证。
连续格上的不动点博弈
提出连续格上的不动点奇偶博弈，统一刻画最小/最大解并推广 progress measure 至格化 µ 演算验证。
交错 bidirected Dyck 可达性的可判定性与复杂度
系统解决交错 bidirected Dyck 可达性的可判定性与复杂度，改进上界并确立可判定与不可判定边界。
通过加速求解无限状态博弈
提出首个带加速技术的无限状态博弈符号半算法，避免传统不动点求解发散并提升求解能力。
面向 Interleaved-Dyck 可达性的快速图简化
提出一种与具体 InterDyck 可达性算法正交的图预处理简化方法，安全删除不贡献交错 Dyck 路径的边，提升精度与可扩展性。
判定差分隐私方案的准确性
提出基于程序不连续性的通用准确性定义，并研究差分隐私方案准确性判定的可判定性与判定过程。
HoCHC：一个反驳完备且语义不变的高阶逻辑模理论系统
为高阶约束 Horn 子句提出简单归结证明系统，并证明其在标准与 Henkin 语义下可靠且反驳完备。
面向运算符优先级语言的模型检测器
提出并实现了首个开源模型检测器 POMC，用于验证运算符优先级语言程序上的 POTL 树结构性质。
面向自动程序验证的 HFL(Z) 有效性检查
提出 HFL(Z) 公式有效性的自动判定方法，配合归约实现对高阶函数式程序各类时序性质的统一全自动验证。
基于偏斜制表的上下文无关语言可达性
提出偏斜制表策略，通过消除递归非终结符产生的冗余摘要边，加速上下文无关语言可达性求解。
有限森林上带复合算子的模态逻辑
证明有限森林上两种带复合算子的模态逻辑的表达力与可满足性复杂度，并解决相关公开问题。
视角博弈（Perspective Games）
提出视角博弈模型，其中玩家仅观察自己拥有的顶点，并研究其获胜策略判定、ATL*模型检测及策略表达能力。
PURLTL：从测试中的不完美轨迹挖掘 LTL 规约
提出 PURLTL，用神经搜索与正例-未标注学习从不完美轨迹挖掘任意 LTL 规约，大幅超越 SOTA。
符号 NetKAT 自动机的主动学习
提出主动学习未知网络 NetKAT 模型（含符号自动机）的算法，并证明其健全性。
带公理的正交逻辑
为带公理的正交逻辑建立证明论，给出广义切消、三次时间判定算法及其与有界宽度消解和 Datalog 扩展的关系。
有限草堆中的无限针：在演绎验证中寻找无限反模型
提出符号结构与模型发现过程，为演绎验证中仅有无穷模型的量词公式找到有限表示的反模型。
基于多重上下文无关语言可达性的程序分析
提出多重上下文无关语言可达性模型，以可调精度、可判定地近似交错 Dyck 可达性，并给出算法复杂度与实现评估。
Axe ’Em：用归纳公理消除伪状态
提出基于归纳公理的可靠精化方法，弥合一阶抽象与良基/有限域语义间的鸿沟，消除伪状态。
有界树宽、多上下文无关文法与向下闭包
证明 MSO 可定义的有界特殊树宽系统语言恰为多上下文无关语言，并用于计算向下闭包。
程序验证算法的原始-对偶视角
提出统一的原始-对偶框架，用广义Lagrangian刻画并设计验证算法，推导已有方法并给出新的不动点逻辑判定算法。
并发随机可达性与安全性博弈中值迭代的停止准则
为并发随机博弈的值迭代提出带上/下界的停止准则，保证近似精度。
通过学习可微迹检查来检验 LTL 可满足性并生成迹
提出可微神经网络方法 VSCNet，将 LTL 可满足性检验与可满足迹生成（SAT-and-GET）统一为神经推理，兼顾精度与效率。
下推正规形式互模拟：一种面向程序等价的名义上下文无关方法
提出下推正规形式互模拟，可可靠、完备且对调用栈无界情形可判定地验证高阶函数式程序上下文等价。
自动程序修复中过拟合的不可判定性
论证过拟合并非测试套件不足导致的可修复缺陷，而是规约缺失下不可判定性的结构性后果。
Cut-Shortcut 全程序指针分析：重新构想无需上下文的上下文敏感分析
提出 Cut-Shortcut，无需上下文即可在指针流图中裁剪不精确边并添加跨方法捷径边，实现快速且精确的 Java 指针分析。
基于高效关系链接的上下文无关语言可达性
提出关系链接视角与 Squid 算法，消除 CFL 可达性求解中的冗余链接操作，显著提升可扩展性。
验证语义引导综合（SemGuS）问题的解
将 SemGuS 解验证归约到 μCLP 有效性，并扩展 SemGuS 以支持非确定性与反应式综合。
DeepSTL
提出 DeepSTL，用文法合成数据训练 Transformer 神经翻译器，将英文非形式化需求自动翻译为信号时序逻辑 STL 规约。
使用句法分离的信号时序逻辑性质的有界模型检测
提出基于句法分离的 STL 有界模型检测算法，将验证归约为 SMT 可满足性，实现有界反驳完备。
可监控性探究：从分支时间到线性时间再返回
建立了带递归 Hennessy-Milner 逻辑的运行时可监控性理论，给出线性时间下可监控片段的表达力层级与监控保证。
线性时序逻辑引导的灰盒模糊测试
提出 LTL-Fuzzer，将灰盒模糊测试扩展到寻找线性时序逻辑性质违反的反例。
借助带优先级与变量的转换器求解含 RegEx 相关函数的字符串约束
提出首个原生支持 RegEx（贪婪/懒惰、捕获组）的字符串理论与求解器，核心为带优先级的流式字符串转换器 PSST。
可解释人工智能的逻辑
提出基于符号逻辑的可解释性语义与计算理论，从决策的必要/充分条件刻画解释。
异步超属性的自动机与不动点
首次提出异步超属性的自动机模型与不动点演算 Hµ，并给出可判定近似分析。
匹配 μ-逻辑
为匹配逻辑给出可靠完备证明系统，并扩展出匹配 μ-逻辑，统一刻画多种不动点、模态与时序逻辑。
模代数数据类型与递归函数求解约束 Horn 子句
提出 IC3 启发的 Racer 算法，在 ADT 与 catamorphism 下求解 CHC，自动合成归纳不变式并保证找到不安全反例。
可配置软件系统中的因果性
提出特征因果性，用反事实推理识别引发系统性质的特征及其交互，并给出计算因果解释的算法。
从模态 μ 演算视角求解奇偶博弈的准多项式时间算法
提出基于 register-index 的奇偶博弈新准多项式求解算法，固定参数下多项式可解。
用于时序验证的模块化原始-对偶不动点逻辑求解
提出模块化原始-对偶方法求解带背景理论的一阶不动点逻辑 µCLP，并将其用于时序验证。
使用位向量自动机的正则表达式匹配
提出位向量自动机（NBVA）模型与算法，使含界重复的正则表达式匹配时间与重复次数上限无关，并实现 BVA-Scan 引擎。
基于导数的、具有回溯语义的真实世界非回溯正则匹配
提出基于导数的非回溯正则匹配算法，支持锚点与计数并保持回溯语义，已在 .NET 7 实现并形式验证。
使用匹配逻辑定义绑定器的一种通用方法
提出用匹配逻辑统一公理化定义对象语言中的绑定器，并给出保守扩展与模型完备性结果。
Innermost 重写的可达性分析
将树自动机补全算法扩展到 innermost 重写策略，以精确近似可达项集合，并在 Timbuk 中实现验证。
通过稳定化求解带长度的字符串约束
提出基于稳定化的字符串约束求解算法，可处理长度约束与不等关系，并集成到 SMT 求解器。
CFL 可达性的次三次证书
证明 CFL 可达性存在 O(n^2) 大小的存在性与非存在性证书，并可在次三次时间内验证。
论理论扩展中的插值与符号消去
研究理论扩展中插值与符号消去的层次化方法，并推广至基理论仅有可量词消去模型完备的情形。
未解释程序的可判定验证
提出 coherent 程序类，使未解释程序的完全自动验证可判定，并可在 Pspace 内完成。
基于 Riesz 空间的概率逻辑
提出 Riesz 模态逻辑，用 Riesz 空间建立概率转移系统性质的对偶理论，并给出可靠完备公理化与概率互模拟刻画。
生命是随机的，时间不是：具有窗口目标的马尔可夫决策过程
将窗口机制扩展到马尔可夫决策过程，解决窗口目标的阈值概率问题并给出通用策略综合方法。
JavaScript 正则表达式的线性匹配
界定了 JavaScript 正则中可线性时间匹配的更大子集，并给出首个非回溯的线性 lookaround 匹配算法。
推断符号自动机
研究符号有限状态自动机（SFA）的可学习性，给出查询学习与极限可识别性的正反条件及规模度量。
高效完全高阶合一
提出高效完全高阶合一过程，通过限制搜索空间与集成片段判定，在 Zipperposition 中实现并优于已有方法。
在线性递推序列上判定 ω-正则性质
证明简单线性递推序列的符号描述几乎周期，并给出判定前缀无关 ω-正则性质的过程。
面向噪声数据的归纳程序合成
提出基于状态加权有限树自动机的框架与算法，在含错误样本的噪声数据上合成正确程序。
Kater：自动化弱内存模型元理论与一致性检查
将弱内存模型元理论问题归约为正则语言包含，并自动生成一致性检查，集成到 GenMC。
RE#：基于导数的高性能正则表达式匹配，支持交、补与受限环视
提出无回溯的正则匹配工具 RE#，基于符号导数支持交、补与受限环视，匹配复杂度对输入线性。
原子层逻辑（Atomic Sheaf Logic）中的等价与条件独立
提出原子层拓扑语义框架，统一解释变量等价与条件独立，并在经典逻辑中验证基本推理原则。
线性时序逻辑与极弱交替自动机的一种高效规范化过程
提出LTL的直接语法规范化过程，得到单指数爆炸的范式，并用于构造确定性Rabin自动机。
不确定性下概率系统模型长期行为的验证
研究在不确定性存在时，对概率系统模型的长期行为进行概率验证，并以概率验证器检验长期性质。
面向模式正则语言的预测性运行时监控
提出面向模式正则语言的预测性运行时监控，能在并发执行重排序中暴露高层时序违规，并给出常空间流式线性时间算法。
论字符串约束的表达能力
系统比较20种字符串约束逻辑理论的语言表达能力，并研究跨理论可表达性的可判定性。
自动化 Dirac 记号中的等式证明
证明 Dirac 记号的一阶理论可判定，并用项重写高效判定等式，实现等价性检查器。
论高阶效应程序的模型检测
将高阶代数效应程序归约为高阶递归方案，并刻画效应处理器下模型检测的可判定边界。
一种拟多项式时间求解奇偶博弈的递归方法
提出 Zielonka 递归算法的改进，将奇偶博弈求解复杂度降至拟多项式时间。
判定单遍堆操作程序的内存安全
将可判定无解释程序扩展到别名感知映射更新，并在森林与单遍条件下判定堆程序内存安全。
逻辑 LTL 博弈的符号化不动点算法
将经典不动点算法推广到符号化逻辑 LTL 博弈，高效合成控制器与获胜策略。
FlexFringe：通过学习概率自动机建模软件行为
FlexFringe 提供高效的概率确定性有限自动机学习实现，可从软件日志学习可解释模型并用于异常检测。
弱内存测试有多难？
证明多种弱内存模型下一致性测试在参数有界时仍 NP 完全，并与 SC、x86-TSO、PSO、Relaxed 形成计算分离。
D<: 的不可判定性及其可判定片段
证明 D<: 的类型检查与子类型不可判定，并给出两个可判定片段与判定算法。
计算概率自动机的概率互模拟距离
将概率互模拟距离刻画为随机博弈解，并给出首个实用的策略迭代计算算法。
共归纳谓词的可表达逻辑
在共代数上为共归纳谓词建立逻辑完全刻画的一般框架，给出充分条件并实例化相似、发散与行为度量。
我的哪些假设对可实现性是不必要的，以及为什么我应当关心？
提出检测并去除反应式系统规约中对可实现性不必要的假设，生成核心规约，从而合成更通用的控制器。
合成 GR(1) 控制器的动态更新
提出并求解 GR(1) 合成控制器的动态更新问题，用桥接控制器实现运行中安全切换至新规约。
论程序分支时间性质验证的逻辑方法的可计算性
揭示多数将分支时间验证归约为逻辑问题的进路，其逻辑问题严格难于验证问题，唯一例外是带不动点的一阶算术有效性。
DSM：一个使用基于循环神经网络语言模型的规约挖掘工具
提出 DSM 工具，用 RNN 语言模型从执行轨迹中挖掘有限状态自动机形式规约。
检查正则表达式消歧鲁棒性的静态分析
提出正则表达式消歧鲁棒性概念，证明判定问题为 PSPACE 完全，并给出实用静态分析算法与优化。
基于模型检测的计时自动机鲁棒性分析
针对时间常数不确定与受扰动的计时自动机，提出若干概念与技术，用模型检测分析其鲁棒性并辅助设计阶段的常数额定。
这不是特性，而是 Bug：从噪声数据中进行容错模型挖掘
提出用 Partial Max-SAT 从含噪执行轨迹中挖掘确定自动机，允许忽略最少故障观测且无需预处理。
快速确定性的黑盒上下文无关文法推断
提出确定性黑盒 CFG 推断方法 TreeVada：按嵌套规则预结构化输入并递归应用学习规则，速度更快、文法质量更高。
黑盒设置下的增量上下文无关文法推断
提出 Kedavra，通过分段示例字符串并增量推断，提升黑盒上下文无关文法推断的质量、速度与可读性。
论一阶逻辑二变量片段中的精确采样
证明 FO2 及其带计数约束扩展在采样意义下具有域可提升性，给出多项式时间精确采样算法。
μ-演算中的规模度量与 α-等价
提出 α-不变的图表示，消除 μ-演算公式因绑定变量重命名导致的指数膨胀，并证明 Fischer-Ladner 闭包大小在 α-等价下不变。
用于 ω-正则验证的超鞅层级
提出超鞅证书层级验证马尔可夫链几乎必然满足 ω-正则性质，证明 DVSSM 最强并给出 LexPMSM 合成算法与工具。
正则模型检测倒置：一种基于不变式的方法
提出基于不变式的自顶向下正则模型检测，用 b-不变式将可达集逼近为正规集并构造自动机验证安全性。
定量性质与自动机的安全性和活性
将布尔安全-活性分类推广到定量性质，并为常见定量自动机给出安全/活性判定、安全闭包与分解。
判定递归程序的异步超属性
提出一种表达力更强的异步超属性逻辑，并在有限状态与下推模型上研究其模型检测复杂度。
有限变量逻辑中的公式学习
提出通用自动机理论技术，在有限变量逻辑中实现语法受限的公式与项精确学习、可实现性判定和合成。
面向健壮性的必要性规约
提出 Necessity 语言，用必要性算子刻画时序蕴含，从功能规约推导健壮性规约并在 Coq 中机械化验证可靠性。
参数化时间自动机中的参数化更新
提出允许时钟更新为参数的时间自动机扩展，并找到一个可判定 EF-空问题、可精确参数综合的语法子类。
几乎每个简单类型 λ 项都有长的 β-归约序列
证明在函数元数与变量数有界时，渐近几乎所有 k 阶简单类型 λ 项都有长达 (k-1) 重指数的 β-归约序列。
论插值算法的完备性
首次系统研究插值算法的完备性，证明若干归结与相继式演算标准插值算法的不完备性及多种完备性。
有限域上概率程序的通用等价与多数性
研究有限域上概率程序等价的可判定性与复杂度，证明通用等价可判定并给出双指数上界。
若干无限状态 MDP 与随机博弈的算法
综述无限状态 Markov 链、MDP 与随机博弈的算法与复杂度，统一递归/计数器式概率程序模型。
零知识中正则表达式等价性的余归纳证明
提出首个正则表达式等价性的零知识证明协议 Crêpe，基于导数与余归纳，可在数秒内验证大规模证明。
精确实数计算的语义、规约逻辑与霍尔逻辑
提出精确实数计算语言 ERC，给出可计算完备的指称语义、可判定规约逻辑及可靠且表达力强的霍尔逻辑。
检查无限下降的复杂性景观
在逻辑无关的抽象框架下，系统刻画循环证明无限下降检查准则的参数化复杂度，并提出改进算法。
递归概率程序时序性质的模型检测
给出概率下推自动机对 ω-可见下推语言（如 CaRet 可描述的性质）模型检测的可判定性与复杂度结果。
具有可判定学习的语言：一个元定理
提出 finite-aspect checkable 语言，并用树自动机元定理统一证明多类表达式学习问题可判定。
EUF 中的一致插值：使用 DAG 表示的算法
提出两种基于项 DAG 表示的算法，用于在 EUF 中计算无量词一致插值，并给出正确性与完备性证明。
带单时钟与初始化时钟依赖概率的概率定时自动机
将单时钟初始化时钟依赖概率定时自动机转为区间MDP，证明其定量与定性可达性可在多项式时间求解。
从示例中学习带约束的 LTL 规约
提出带约束的 LTL 学习问题，用一阶关系逻辑编码并归约到 MaxSAT，实现 ATLAS 工具。
最小历史确定性 co-Büchi 自动机：同余与被动学习
用同余刻画最小历史确定性 co-Büchi 自动机，并给出多项式时间被动学习算法。
仿射连续 VASS 判定问题的可判定性与复杂度
本文对仿射连续 VASS 的可达、覆盖与状态可达问题给出近乎完全的可判定性分类与紧复杂度界。
线性终止是不可判定的
通过从希尔伯特第十问题归约，证明单规则重写系统线性解释终止性不可判定，并扩展至多种序与多项式解释。
Perspective 多玩家博弈
将 Perspective 博弈扩展到多玩家、联盟与非零和，证明不可判定边界，并给出两人非零和可判定与理性合成结果。
基于加权自动机的精确字符串约束解计数
提出加权自动机模型对字符串约束解计数，保持与输入字符串值的一一对应，修正传统自动机模型的计数错误。
面向 UNSAT 的基于归结的交互式证明系统
将竞争性交互证明归约为算术化问题，并给出首个与 Davis-Putnam 归结竞争的 UNSAT 交互协议。
基于关系式 NetKAT 的网络变更验证
提出 Relational NetKAT 规格语言与转换器/自动机算法，以验证网络变更是否符合意图。
模群（Groups）的同余闭包
提出模群公理的同余闭包框架，通过等式完成过程构造基收敛重写系统，并在终止时判定相关字问题。
符号自动机：模理论下的 ω-正则性
将符号自动机从有限字推广到 ω-正则语言，统一交替/非确定 Büchi 自动机与 LTL、PSL 的模理论框架。
论简单类型 lambda 演算的可判定与不可判定扩展
给出 finitary PCF 四种扩展不可判定性的简单证明，并用类型系统刻画含引用单元的可判定片段。
马尔可夫决策过程中概率提升因果性的基础
为 MDP 中基于概率提升的因果关系奠定数学基础，并分析其算法与复杂度。
历史确定性的时间自动机
证明历史确定性时间自动机严格介于确定性与非确定性之间，并使其 universality、inclusion 与 synthesis 判定为 EXPTIME 完全。
符号化的 Parikh 定理
为符号自动机与文法提出多项式时间构造，将 Parikh 计数抽象编码为存在 Presburger 公式，避免指数爆炸。
基于内在定义的可预测验证
提出用满足局部条件的 monadic maps 定义数据结构，实现可预测的验证。
V-Star：从程序输入中学习可见下推文法
提出 V-Star，用可见下推自动机主动学习，从样本输入推断程序输入文法的嵌套结构，并学习 S-表达式、JSON、XML。
高阶性质导向可达性
提出 PDR 的高阶扩展 HoPDR，用于高阶递归函数描述的系统及高阶程序安全性质验证。
函数式程序性质的一阶完备推理
将函数式程序验证中展开递归定义加SMT无量词推理的启发式，推广为组合一阶理论上的完备推理技术。
双人可达性博弈的顽固集约简
提出双人可达性博弈的顽固集偏序约简理论，正确剪枝双方交错，并在TAPAAL中实现加权Petri网博弈约简。
最小计算集合论中的适用数学
扩展静态逻辑框架，证明最小谓词主义无限集理论是计算性的，且足以形式化大部分科学适用数学。
非确定性与概率 Büchi 自动机的公平模拟：一个余代数视角
从余代数视角统一推广 Büchi 自动机的公平模拟至非确定树自动机与概率字自动机，并证明其可靠性。
面向 GR(1) 可实现性检查的演化感知启发式方法
提出演化感知的 GR(1) 可实现性检查启发式，复用先前检查的中间数据加速迭代开发中的检查。
马尔可夫模型中的乘性奖励
研究马尔可夫链与MDP中乘性奖励期望值/最优值的计算问题，给出复杂度刻画与算法。
最好不要一起：上下文无关语言可达性的分阶段求解
提出分阶段求解 CFL 可达性，将文法分解为括号匹配 CFG 与控制/数据流正则文法，大幅加速程序分析。
论概率下推自动机中的证书、期望运行时间与终止性
揭示概率下推自动机证书存在性与期望终止时间的联系，并给出正几乎必然终止的易验证证明。
超越上下文无关的概率验证
证明受限概率树栈自动机的几乎必然终止与ω-正则模型检测可判定，并对应概率 MAHORS。
死锁避免的分布式控制器合成
提出两种限制使带锁系统的分布式死锁避免控制器合成可判定，并刻画其精确复杂度。
导数引导的符号执行
提出符号导数引导的符号执行，借助 LTLf 规约与符号自动机剪枝，高效证伪带不透明库的程序中数据结构安全性质。
验证反应式系统中的异步超属性
提出博弈式方法验证反应式系统中的任意 ∀*∃* 异步 HyperLTL 公式，并给出有限状态判定片段与原型实现。
带测试与顶元素的 Kleene 代数的完备性定理
证明了带测试与顶元素的 Kleene 代数的两个完备性定理，并给出二元关系等式理论的 PSpace 算法。
不动点理论——颠倒视角
提出证明元素高于最大不动点或低于最小不动点的证明规则，并用有限逼近与 MV-代数格统一处理概率/度量语义及随机博弈。
面向 Eilenberg--Moore 代数的代数语言理论
提出基于 Eilenberg--Moore 代数的代数语言理论，支持无限多 sort 的代数并借助可定义代数连接逻辑。
概率高阶不动点逻辑（PHFL）
提出概率高阶不动点逻辑 PHFL，证明其表达力与模型检测的不可判定性，并用类型系统刻画可判定片段。
通过解析系统化字符串编辑变异来学习黑盒系统的词法结构
对输入串施加系统化编辑变异并解析黑盒系统响应，以推断其词法结构。
黑盒环境下复杂编程语言的上下文无关文法推断
提出 Crucio，通过分解森林与分布矩阵从黑盒样本中为 C/C++/Java 等复杂语言高效推断上下文无关文法。
线性时序反例中的因果检测
提出 LTL 反例的合取式因果定义与计算算法，改进模型检测反例诊断。
EffBT：一种高效的行为树反应式合成与执行框架
提出 EffBT，从 GR(1) 规约自动合成语义正确且高效执行的行为树，并引入剪枝与 Parallel 节点优化执行。
如果起初不成功：通过多次执行扩展可监控性
研究利用多次系统运行监控分支时间性质，证明可系统扩展传统可监控性边界并给出运行次数界。
特征与特征交互的黑盒可观测性
提出黑盒可观测性概念与判定程序，判断特征及其交互效应能否通过配置黑盒观测被隔离。
通过嵌套数据的状态与控制情境等价
证明有限无递归的 ML 风格语言中一阶引用与续延程序的情境等价可判定，并归约为嵌套数据自动机等价。
单射分段仿射映射的可达性
证明单射的一维两区间分段仿射映射可达性可判定，并揭示相关问题的丢番图与拓扑性质。
验证常速率多模式系统的线性时序规范
为常速率多模式系统引入 LTL 变体，并刻画其模型检测片段的复杂度版图：P-完全、NP-完全或不可判定。
在压缩轨迹上以多项式时间检查 LTL[F,G,X]
提出直接检查压缩执行轨迹上 LTL[F,G,X] 性质的多项式时间算法，避免先解压。
责任与验证：时序逻辑中的重要性值
将 Shapley 值引入模型检测，度量系统组件对满足时序规约的重要性，并给出线性与分支时序逻辑下的复杂度上下界。
在马尔可夫决策过程中混合概率与非概率目标
研究MDP中布尔组合的概率与非概率ω-正则目标，给出策略存在性算法和复杂度界。
不完美信息 ATL 的 Hennessy-Milner 定理
为不完美信息 ATL 建立基于历史的交替互模拟与共同知识语义之间的完整 Hennessy-Milner 定理，并证明相关互模拟不可判定。
最优重写公式与数据库查询：项重写、结构分解与复杂度的交汇
该论文为正向一阶公式在常见等价保持重写规则下的宽度最小化给出完备算法，连接项重写、查询求值与结构分解。
轨道闭包与矩阵群的判定问题
给出判定一个簇是否为 s-生成交换代数矩阵群作用下点轨道闭包的多项式空间算法。
结构约简与 stutter 敏感性质
提出 shortening/lengthening 不敏感语言以推广 stutter 不敏感，并给出基于结构约简的半判定验证。
面向小样本学习的 DSL 合成
研究符号域中小样本学习的 DSL 合成问题，证明其可判定性并给出正则树表征。
宽度无关位向量谓词的已验证判定过程
在 Lean 中机械化模型检测与 MBA-Blast 算法，为宽度无关位向量谓词提供可扩展的已验证判定过程。
正则约束传播的力量
提出并实现正则约束传播方法，可可靠且完备地求解一大类字符串约束，并显著提升 OSTRICH 求解器性能。
分析噪声存在下 Angluin L* 算法的鲁棒性
实验分析 Angluin L* 的噪声鲁棒性：随机噪声下表现良好、结构化噪声下较差，并证明随机过程几乎必然产生非递归可枚举语言。
为 ω-正则语言接受器构造简洁的特征样本
证明非确定性 ω-自动机无多项式规模特征样本，并为完全信息化的确定性 ω-自动机给出多项式时间构造与学习算法。
高阶 MSL Horn 约束
提出高阶 MSL Horn 约束类并给出基于消解的判定过程，证明其与 HORS 模型检测可相互归约，并应用于高阶程序验证。
Riesz 空间与模态 Riesz 空间的证明论
为 Riesz 空间与模态 Riesz 空间设计超序列演算，证明可靠、完备与切消，并据此给出模态 Riesz 空间可判定性的新证明。
Coq 中的希尔伯特第十问题（扩展版）
在 Coq 中完成 DPRM 定理的首次完整机器化证明，形式化了希尔伯特第十问题的不可判定性。
定量验证中的比较器自动机
提出比较器自动机，统一比较两条无限权重序列的聚合值，并用于定量验证算法。
概率语义下的定量自动机
证明 monitor counter 自动机与嵌套加权自动机等价，并刻画其在概率语义下的可判定性与复杂度。
多宽度参数化位向量的可靠且完备求解：基于原则性归约
将多宽度参数化位向量归约为单宽度公式，实现可靠完备的高效求解与自动机判定。
使用自动机验证 Repeat-until-Success 协议
提出基于层同步树自动机的全自动框架，验证 RUS 量子协议的功能正确性并发现文献中的新 bug。
EUFⁿ：未解释函数等式理论的一个可判定扩展
将 EUF 扩展为支持参数化复合深度的 EUFⁿ，并用条件同余图给出可判定性与复杂度上界。
超越规约符合性：一种验证利益相关者期望的逻辑
提出语义期望逻辑 SEL，将利益相关者期望形式化并量化，以弥补规约符合性验证无法发现的验证鸿沟。
语言学理论与时序逻辑中的误形式化相吻合
分析LTL规格形式化错误，发现语言学现象可解释近半新手与多数专家错误。
可达性条件下的初始代数对应
提出统一范畴框架，用伴随刻画可达性条件，使转移系统的两种不动点/初始代数语义一致，并实例化到马尔可夫链与自动机。
线性动力系统中的多重可达性
证明线性动力系统多重可达性在 d=10、m=9 时不可判定，并给出二维平面中旋转矩阵与半平面目标的可判定性。
重置工作流网的健全性
证明重置工作流网的广义健全性不可判定，并提出介于1-健全性与广义健全性之间的可判定性质“1-in-between健全性”。
类型自动机
提出类型自动机，以程序类型为控制与存储，连接类型系统与自动机理论并支持类型级元编程。
关系霍尔逻辑的对齐完备性
提出对齐完备性概念，用归纳断言法与乘积自动机刻画关系霍尔逻辑的规则完备性。
概率验证中的符号时间与空间权衡
提出更快的符号算法计算 MDP 的最大端分量分解，给出符号操作与空间权衡，解决长期开放问题。
HyperLTL 的异步扩展
提出 HyperLTL 的两种异步正交扩展 HyperLTLS 与 HyperLTLC，证明一般模型检测不可判定并给出可判定片段及复杂度。
机器空间 I：弱指数与紧空间上的量化
引入机器空间区分可验证性质与其验证过程，构造弱指数，并给出紧空间上全称量化的拓扑算法。
在分离逻辑的极小片段中编码 Peano 算术
将 Peano 算术 Π⁰₁ 公式编码到仅含直觉 points-to、0 与后继的分离逻辑片段，证明有效性等价与不可判定。
几乎可交换迁移系统的上下文无关语言可达性
将 CFL 可达性推广到几乎可交换迁移系统，证明其同态像半线性并给出多项式时间 Presburger 构造。
RAT-CAT-SAT：内存一致性模型的模型检测
提出 RAT-CAT-SAT，用关系逻辑可满足性与循环证明系统对 CAT 内存一致性模型进行模型检测。
基于单调不动点复用的高效增量 GR(1) 合成
提出增量 GR(1) 合成，通过复用获胜区域与单调不动点加速可实现性检查。
EREQ：带量词的正则表达式与增量式量词消去
提出带量词正则表达式 EREQ，以符号导数做增量式量词消去，替代自动机确定化并高效判定 wMSO。
TSO 博弈——总存储序语义下安全博弈的可判定性（含附录的扩展 LMCS 版本）
将 TSO 语义扩展为回合制双人安全博弈，并给出不同缓冲区刷新责任下可判定性的完整图谱。
语义正则表达式的成员测试
研究语义正则表达式（SemREs）的成员测试问题，即判定字符串是否匹配带外部 oracle 查询的正则模式。
面向超安全验证的递归程序乘积
提出递归乘积程序构造框架，将无限状态递归程序的超安全验证归约为标准安全验证。
连续 Petri 网中的分离器
证明连续 Petri 网的不可达性可由多项式时间可构造的局部闭分离器见证，并可在 NC 内验证该证书。
从停机问题到半合一的构造性多一归约（扩展版）
给出停机问题到半合一的构造性多一归约，并用无公理 Coq 机械化证明其 RE 完全性。
通过因子分解系统与实例的极小性概念
在带因子分解系统的范畴中统一刻画余代系统的极小性与最小化，并给出可达性与可观测性最小化及可顺序化条件。