重写框架中的符号抽象契约综合
编程语言
2016-08-22 v1 计算机科学中的逻辑
摘要
我们提出一种自动化技术，用于从用C语言的一个非平凡子集（称为KernelC，支持基于指针的结构和堆操作）编写的程序中推断软件契约。从KernelC在K框架中的语义定义出发，我们用基于抽象包含的新型断言综合能力丰富了K最近提供的符号执行设施。粗略地说，我们定义了一种抽象符号技术，通过使用同一程序中的其他（观察器）例程来解释（修改器）C函数的执行。我们在自动化工具KindSpec 2.0中实现了我们的技术，该工具通过定义C例程精确的输入/输出行为来生成表达前置和后置条件断言的逻辑公理。
引用
@article{arxiv.1608.05619,
title = {Symbolic Abstract Contract Synthesis in a Rewriting Framework},
author = {María Alpuente and Daniel Pardo and Alicia Villanueva},
journal= {arXiv preprint arXiv:1608.05619},
year = {2016}
}
备注
Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)