文章目录

• 前言
• 正文
• • 程序综合
  • 枚举法
  • • CEGIS：基于反例的优化
  • 约束求解法
  • 启发式搜索法
  • 统计法
  • 基于组件的程序综合 Component-Based Synthesis
• 小结
• 参考文献

前言

创作开始时间：

如题，学习一下程序综合 Program Synthesis的相关知识。参考：熊英飞老师2018《软件分析》课件。

正文

程序综合

程序综合是软件分析问题。
程序综合作为搜索问题。

目前大多数程序综合技术都只处理表达式，因为可以直接转成约束让SMT求解。

• 枚举法：按照固定格式搜索
• 约束求解法：将程序搜索问题整体转成约束求解问题
• 启发式搜索法：采用启发式搜索
• 统计法：采用机器学习等方法寻找概率最高的程序

枚举法

按语法依次展开：

• 自顶向下遍历
• 自底向上遍历
• 双向搜索：要求能计算最强后条件或者最弱前条件，通常用于 pipeline 程序或者系统状态固定的程序

判断程序是否等价：

• 通过 SMT 求解器可以判断，但是编码比较麻烦
• 通过预定义规则判断

CEGIS：基于反例的优化

约束求解较慢，执行测试较快。将约束求解器返回的反例作为测试输入保存。

优化一：验证的时候首先采用测试验证
优化二：判断等价性的时候首先采用测试的结果判断

约束求解法

将程序综合问题整体转换成约束求解问题，由SMT 求解器求解。

基于构件的程序综合

启发式搜索法

统计法

这个有点像马尔科夫链。

基于组件的程序综合 Component-Based Synthesis

参考：

• https://www.cs.cmu.edu/~aldrich/courses/17-665/notes/notes13-synthesis.pdf

先了解Oracle-guided synthesis：

原来如此，讲的挺好的。例子也很好懂。

是通过SMT问题，得到反例Counterexample，然后再加入到Specification里面，从而不断强化specification。

看完这个之后再看：

• 【ICSE 13论文】SemFix: Program repair via semantic analysis

就大概能看懂了。

小结

还是学到了很多的，后续再补充完善。

创作结束时间：2022年11月16日23:42:19

参考文献

• https://www.cs.cmu.edu/~aldrich/courses/17-355-18sp/notes/notes13-synthesis.pdf