公开(公告)号：CN107180193B

公开(公告)日：2020-03-27

申请号：CN201710480725.9

申请日：2017-06-22

Applicant: 南京大学

Inventor： 卜磊 ,  李一超 ,  陶昱天 ,  闾乐成 ,  梁东隽 ,  沈大川 ,  赵建华 ,  李宣东

IPC: G06F21/56

Abstract: 本发明公开了一种将程序代码转换成数据约束的方法和装置。该方法首先将程序代码转换成中间指令集，然后将中间指令集进行细化拆分，细化拆分时将原变量定义指令中涉及的复杂类型的变量细化拆分成多个简单类型的变量，然后将简单类型的变量再进一步细化成简单类型的地址指针变量和简单类型的指针指向变量，最后再将相应的变量定义指令细化拆分成针对简单类型的地址指针变量和简单类型的指针指向变量的内存分配指令和初始化数据存储指令，然后提取细化拆分后的中间指令集中的存取指令、算术指令和比较指令作为数据约束。

公开(公告)号：CN107180193A

公开(公告)日：2017-09-19

申请号：CN201710480725.9

申请日：2017-06-22

Applicant: 南京大学

Inventor： 卜磊 ,  李一超 ,  陶昱天 ,  闾乐成 ,  梁东隽 ,  沈大川 ,  赵建华 ,  李宣东

IPC: G06F21/56

Abstract: 本发明公开了一种将程序代码转换成数据约束的方法和装置。该方法首先将程序代码转换成中间指令集，然后将中间指令集进行细化拆分，细化拆分时将原变量定义指令中涉及的复杂类型的变量细化拆分成多个简单类型的变量，然后将简单类型的变量再进一步细化成简单类型的地址指针变量和简单类型的指针指向变量，最后再将相应的变量定义指令细化拆分成针对简单类型的地址指针变量和简单类型的指针指向变量的内存分配指令和初始化数据存储指令，然后提取细化拆分后的中间指令集中的存取指令、算术指令和比较指令作为数据约束。

公开(公告)号：CN108804135B

公开(公告)日：2020-02-07

申请号：CN201810426842.1

申请日：2018-05-07

Applicant: 南京大学

Inventor： 卜磊 ,  沈大川 ,  庄媛 ,  李宣东

IPC: G06F8/72 ,  G06F8/30 ,  G06N3/12

Abstract: 本发明公开了一种基于目标规约满足度评估的符合规约并发程序合成方法和装置。该方法或装置通过将用户提供的线性时序逻辑规约转换成限界线性时序逻辑规约，然后使用统计模型检验工具评估候选者满足规约的概率，计算每个候选者的适应度，然后再根据该适应度采用遗传算法得到新的候选程序，避免了模型检验工具直接逐个检验候选程序，从而提高程序合成的生成效率。

公开(公告)号：CN108804135A

公开(公告)日：2018-11-13

申请号：CN201810426842.1

申请日：2018-05-07

Applicant: 南京大学

Inventor： 卜磊 ,  沈大川 ,  庄媛 ,  李宣东

IPC: G06F8/72 ,  G06F8/30 ,  G06N3/12

Abstract: 本发明公开了一种基于目标规约满足度评估的符合规约并发程序合成方法和装置。该方法或装置通过将用户提供的线性时序逻辑规约转换成限界线性时序逻辑规约，然后使用统计模型检验工具评估候选者满足规约的概率，计算每个候选者的适应度，然后再根据该适应度采用遗传算法得到新的候选程序，避免了模型检验工具直接逐个检验候选程序，从而提高程序合成的生成效率。