使用线性代数与约束求解的有序排序一阶理论模型合成
编程语言
2015-12-23 v1 计算机科学中的逻辑
摘要
声明式程序终止性分析的最新进展强调，将表示相关程序的逻辑理论的适当模型用作证明声明式程序终止性的通用方法。在此背景下，有序排序一阶逻辑提供了一个表示声明式程序的强大框架。它也提供了一个目标逻辑，通过变换获得其他逻辑的模型。我们研究有序排序一阶逻辑的数值模型的自动生成及其在程序分析中的使用，特别是在声明式程序的终止性分析中。我们使用凸域为有序排序签名的不同排序赋予域；我们通过适当调整的凸矩阵解释来解释排序签名中的秩符号。此类数值解释允许使用来自线性代数和算术约束求解的现有算法和工具来合成模型。
引用
@article{arxiv.1512.06943,
title = {Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving},
author = {Salvador Lucas},
journal= {arXiv preprint arXiv:1512.06943},
year = {2015}
}
备注
In Proceedings PROLE 2015, arXiv:1512.06178