协同偏序归约与状态内插的框架
计算机科学中的逻辑
2014-08-06 v1 编程语言
摘要
我们解决了并发程序安全验证中交错推理的问题。文献中有两种突出的剪枝搜索空间的技术。首先，有经过充分研究的基于迹的方法，统称为“偏序归约”（POR），通过将迹的过渡全序抽象为偏序来弱化迹的概念。其次，有基于状态的内插，其中一组公式可以通过考虑要验证的性质进行泛化。我们的主要贡献是一个框架，将POR与状态内插协同结合，使得整体效果大于部分之和。
引用
@article{arxiv.1408.0957,
title = {A Framework to Synergize Partial Order Reduction with State Interpolation},
author = {Duc-Hiep Chu and Joxan Jaffar},
journal= {arXiv preprint arXiv:1408.0957},
year = {2014}
}