认证符号执行中的证明携带参数：以反合一为例

符号执行使用多种算法（匹配、（反）合一），其执行过程作为证明对象生成的参数。本文提出一种为此类参数生成证明对象的通用方法。我们详细展示该方法在反合一情形下的工作机制。该方案配有实现原型，包括证明对象生成器与证明对象检查器。为考察证明对象规模，我们针对受C与Java的K定义启发的输入生成并检查了证明对象。