μZ- An Efficient Engine for Fixed Points with Constraints
μZ- An Efficient Engine for Fixed Points with Constraints
复制标题
μZ——具有约束的定点高效引擎
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
L. D. Moura
中科院分区：
文献类型：
--
作者：
Krystof Hoder;Nikolaj S. Bjørner;L. D. Moura
µZ工具是一个可扩展的高效引擎，适用于具有约束的固定点。它支持内置域和插件域的组合上的高级声明性定点约束。内置域包括呈现给SMT求解器Z3的公式和从抽象解释已知的域。我们将介绍µZ的接口、一些域，以及一组示例来说明µZ的使用。
The µZ tool is a scalable, efficient engine for fixed points with constraints. It supports high-level declarative fixed point constraints over a combination of built-in and plugin domains. The built-in domains include formulas presented to the SMT solver Z3 and domains known from abstract interpretation. We present the interface to µZ, a number of the domains, and a set of examples illustrating the use of µZ.