A fixpoint calculus for local and global program flows
A fixpoint calculus for local and global program flows
复制标题
局部和全局程序流的不动点演算
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
P. Madhusudan
中科院分区：
文献类型：
--
作者：
R. Alur;Swarat Chaudhuri;P. Madhusudan
我们定义了一种新的不动点模态逻辑——可见下推μ演算（VP - μ），它是模态μ演算的扩展。该逻辑的模型是结构化程序的执行树，其中过程调用和返回清晰可见。这种新逻辑能够表达其经典对应逻辑在模型上无法表达的下推规范，其灵感源自近期关于可见下推语言的研究[4]。我们证明，该逻辑自然地涵盖了程序验证和数据流分析中若干有趣的程序规范。这包括各种程序规范，例如计算局部和全局程序流的组合、过程的前置/后置条件、涉及上下文栈的安全属性以及过程间数据流分析属性。该逻辑能够实现流敏感和过程间分析，并且具有允许跳过过程调用的结构，以便也能追踪过程中的局部流。通过将摘要而非节点视为一等对象，并采用适当的结构来连接摘要，该逻辑对模态μ演算的语义进行了推广，自然地体现了下推模型的模型检查方式。本文的主要成果是，针对下推模型，VP - μ的模型检查问题能够有效解决，且所需工作量并不比诸如CTL等较弱逻辑更多。我们还研究了VP - μ逻辑的表达能力：我们表明它涵盖了线性结构上相应下推时态逻辑（^[2]）以及经典μ演算所表达的所有属性。这使得VP - μ成为已知的最具表达力且算法软件模型检查可行的程序逻辑。事实上，大多数已知程序逻辑（μ演算、时态逻辑LTL和CTL、^等）的可判定性可以通过它们在树的一元二阶逻辑中的解释来理解。但对于VP - μ逻辑并非如此，这使其成为一种新的强大且易处理的程序逻辑。
We define a new fixpoint modal logic, the visibly pushdown μ-calculus (VP-μ), as an extension of the modal μ-calculus. The models of this logic are execution trees of structured programs where the procedure calls and returns are made visible. This new logic can express pushdown specifications on the model that its classical counterpart cannot, and is motivated by recent work on visibly pushdown languages [4]. We show that our logic naturally captures several interesting program specifications in program verification and dataflow analysis. This includes a variety of program specifications such as computing combinations of local and global program flows, pre/post conditions of procedures, security properties involving the context stack, and interprocedural dataflow analysis properties. The logic can capture flow-sensitive and inter-procedural analysis, and it has constructs that allow skipping procedure calls so that local flows in a procedure can also be tracked. The logic generalizes the semantics of the modal μ-calculus by considering summaries instead of nodes as first-class objects, with appropriate constructs for concatenating summaries, and naturally captures the way in which pushdown models are model-checked. The main result of the paper is that the model-checking problem for VP-μ is effectively solvable against pushdown models with no more effort than that required for weaker logics such as CTL. We also investigate the expressive power of the logic VP-μ: we show that it encompasses all properties expressed by a corresponding pushdown temporal logic on linear structures (caret [2]) as well as by the classical μ-calculus. This makes VP-μ the most expressive known program logic for which algorithmic software model checking is feasible. In fact, the decidability of most known program logics (μ-calculus, temporal logics LTL and CTL, caret, etc.) can be understood by their interpretation in the monadic second-order logic over trees. This is not true for the logic VP-μ, making it a new powerful tractable program logic.