同步代码的模块化不变式合成
计算机科学中的逻辑
2014-12-04 v1
摘要
本文探索了多种为编码为Horn子句的同步代码合成模块化不变式的技术。模块化不变式是一组表征谓词有效性的公式，在分析、综合、测试和程序转换的不同方面非常有用。我们描述了两种为用同步数据流语言Lustre编写的代码生成模块化不变式的技术。第一种技术直接以模块化方式编码同步代码。而在第二种技术中，我们从整体不变式出发合成模块化不变式。两种技术都利用了基于属性导向可达性的分析技术。我们还描述了一种最小化合成不变式的技术。
引用
@article{arxiv.1412.1152,
title = {Synthesizing Modular Invariants for Synchronous Code},
author = {Pierre-Loic Garoche and Arie Gurfinkel and Temesghen Kahsai},
journal= {arXiv preprint arXiv:1412.1152},
year = {2014}
}
备注
In Proceedings HCVS 2014, arXiv:1412.0825