可靠的up-to技术与完备的抽象域
计算机科学中的逻辑
2018-05-03 v2
摘要
抽象解释是一种自动寻找程序或代码片断不变量（其语义通过最小不动点给出）的方法。Up-to技术被引入作为余归纳（一种通过最大不动点证明性质的抽象原理）的增强。虽然抽象解释根据定义总是可靠的，但up-to技术的可靠性需要一些技巧来证明。对于完备性，情况则相反：up-to技术总是完备的，而抽象域则不是。在这项工作中，我们展示了在合理假设下，可靠的up-to技术与完备的抽象域之间存在明显的联系。
引用
@article{arxiv.1804.10507,
title = {Sound up-to techniques and Complete abstract domains},
author = {Filippo Bonchi and Pierre Ganty and Roberto Giacobazzi and Dusko Pavlovic},
journal= {arXiv preprint arXiv:1804.10507},
year = {2018}
}
备注
12 pages, accepted to 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'18)