一句话：提出将 C 程序反转的技术，使现有前向可达性分析方法能反向执行，以更高效地分析错误位置可达性。
错误可达性分析用于判断程序中的错误位置能否从初始状态到达，是软件验证的核心问题。传统方法通常沿前向方向分析，但在某些情况下，从错误位置出发进行反向可达性分析可能更高效。本文提出一种反转 C 程序的技术，使已有的前向可达性分析方法能够以反向方式遍历原程序，从而复用现有验证基础设施。该技术将实现为独立工具，便于集成到现有验证工具的流水线中。摘要未报告具体实验结果或性能数据，因此其关键贡献在于方法设计与工具集成思路。
Reachability analysis, used to determine whether an error location in a program is reachable from the initial state, is a key problem in software verification. While standard techniques typically perform this analysis in the forward direction, analyzing reachability backward from the error location can be more efficient in some instances. This research introduces a technique for reversing C programs, allowing existing forward reachability methods to effectively traverse the original program in reverse. The technique will be implemented as a standalone tool that can be easily integrated into the pipelines of existing verification tools.