Numerical Invariants via Abstract Machines
Numerical Invariants via Abstract Machines
复制标题
通过抽象机的数值不变量
DOI：
10.1007/978-3-319-99725-4_3
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Zachary Kincaid
中科院分区：
文献类型：
--
作者：
Zachary Kincaid
本文概述了最近的一系列工作产生的非线性数值不变量的循环和递归程序。该方法是组合的，因为它通过将程序分解为多个部分，独立分析每个部分，然后组合结果来操作。最根本的挑战是设计一种有效的方法来分析给定的分析其主体的结果的循环的行为。其核心思想是将问题分解为两个部分：首先用一个抽象机来近似回路动力学，然后符号化地计算抽象机的可达关系。
This paper presents an overview of a line of recent work on generating non-linear numerical invariants for loops and recursive procedures. The method is compositional in the sense that it operates by breaking the program into parts, analyzing each part independently, and then combining the results. The fundamental challenge is to devise an effective method for analyzing the behavior of a loop given the results of analyzing its body. The key idea is to separate the problem into two: first we approximate the loop dynamics by an abstract machine, and then symbolically compute the reachability relation of the abstract machine.