创作开始时间：
如题，学习一下程序综合 Program Synthesis的相关知识。参考：熊英飞老师2018《软件分析》课件。
程序综合是软件分析问题。
程序综合作为搜索问题。
目前大多数程序综合技术都只处理表达式，因为可以直接转成约束让SMT求解。
按语法依次展开：
判断程序是否等价：
约束求解较慢，执行测试较快。将约束求解器返回的反例作为测试输入保存。
优化一：验证的时候首先采用测试验证
优化二：判断等价性的时候首先采用测试的结果判断
将程序综合问题整体转换成约束求解问题，由SMT 求解器求解。
基于构件的程序综合
参考：
先了解Oracle-guided synthesis：
是通过SMT问题，得到反例Counterexample，然后再加入到Specification里面，从而不断强化specification。
看完这个之后再看：
就大概能看懂了。
还是学到了很多的，后续再补充完善。
创作结束时间：2022年11月16日23:42:19