【软件分析第17讲-学习笔记】程序综合 Program Synthesis

前言

创作开始时间：

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

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

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

按语法依次展开：

判断程序是否等价：

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

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

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

基于构件的程序综合

在这里插入图片描述

在这里插入图片描述

在这里插入图片描述
这个有点像马尔科夫链。

参考：

先了解Oracle-guided synthesis：
在这里插入图片描述
原来如此，讲的挺好的。例子也很好懂。

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

看完这个之后再看：

就大概能看懂了。

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

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

相关阅读:
Linux性能监控命令_pidstat & 统计进程信息
STM32开发——感应垃圾桶（舵机、超声波测距、振动检测）
深度学习网路模型
伪元素和伪类的概念和区别
新书推荐——华为·无线局域网应用技术（微课版丨第2版）
ubuntu 24.04 beta server NAT模式上网设置
spring mvc源码分析之请求分发
Java WebSocket服务在多tomcat服务下怎么进行互通，websocket多服务负载均衡下怎么进行交互，websocket客户端调用实例
golang常用库之-操作redis go-redis/redis库、 go-redsync/redsync库（redis分布式锁）
8.11 Day39----框架面试题

原文地址：https://blog.csdn.net/weixin_39278265/article/details/127894029