Refinement Type Inference via Horn Constraint Optimization
Refinement Type Inference via Horn Constraint Optimization
复制标题
通过 Horn 约束优化进行细化类型推断
DOI：
10.1007/978-3-662-48288-9_12
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Hiroshi Unno
中科院分区：
文献类型：
--
作者：
Kodai Hashimoto;Hiroshi Unno
提出了一种推断高阶函数程序精化类型的新方法。所提出的方法的主要优点是它可以根据用户指定的偏好顺序推断出最大首选（即，帕累托最优）细化类型。所提出的方法支持的细化类型的灵活优化为有趣的应用程序铺平了道路，例如推断给定程序满足（或违反）给定安全（或终止）属性的输入的最一般特征。该方法采用一种新的细化类型系统，可以灵活地对程序中的不确定性进行推理，从而将此类类型优化问题简化为霍恩约束优化问题。然后，我们的方法通过基于模板的不变量生成反复改进当前解直至收敛来解决约束优化问题。我们已经在此基础上实现了一个原型推理系统，并在初步实验中取得了令人满意的结果。
We propose a novel method for inferring refinement types of higher-order functional programs. The main advantage of the proposed method is that it can infer maximally preferred (i.e., Pareto optimal) refinement types with respect to a user-specified preference order. The flexible optimization of refinement types enabled by the proposed method paves the way for interesting applications, such as inferring most-general characterization of inputs for which a given program satisfies (or violates) a given safety (or termination) property. Our method reduces such a type optimization problem to a Horn constraint optimization problem by using a new refinement type system that can flexibly reason about non-determinism in programs. Our method then solves the constraint optimization problem by repeatedly improving a current solution until convergence via template-based invariant generation. We have implemented a prototype inference system based on our method, and obtained promising results in preliminary experiments.
登录
查看更多内容
HMC：使用抽象解释器验证功能程序
DOI：
--
发表时间：
2010
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
Ranjit Jhala;R. Majumdar;A. Rybalchenko
通讯作者：
A. Rybalchenko
DOI：
10.1007/978-3-642-54833-8_21
发表时间：
2014-04
期刊：
--
影响因子：
--
作者：
Takuya Kuwahara;Tachio Terauchi;Hiroshi Unno;N. Kobayashi
通讯作者：
Takuya Kuwahara;Tachio Terauchi;Hiroshi Unno;N. Kobayashi
DOI：
10.1145/2429069.2429081
发表时间：
2013-01
期刊：
--
影响因子：
--
作者：
Hiroshi Unno;Tachio Terauchi;N. Kobayashi
通讯作者：
Hiroshi Unno;Tachio Terauchi;N. Kobayashi
SAT 模理论与最优化问题
DOI：
--
发表时间：
2006
期刊：
International Conference on Theory and Applications of Satisfiability Testing
影响因子：
--
作者：
R. Nieuwenhuis;Albert Oliveras
通讯作者：
Albert Oliveras
解决存在量化的喇叭子句
DOI：
10.1007/978-3-642-39799-8_61
发表时间：
2013
期刊：
影响因子：
--
作者：
Tewodros A. Beyene;Corneliu Popeea;Andrey Rybalchenko
通讯作者：
Andrey Rybalchenko