Static Analysis Based on Model Checking

9970679堪萨斯州立大学大卫·A·施密特基于模型检查的静态分析这个项目旨在集成基于时态逻辑、程序控制流分析和数据流分析的技术，并将结果应用于验证基于对象和基于函数的程序的正确性和安全性属性。这项工作将分两个阶段进行。首先，将发展和加强Steffen发现的程序数据流分析和程序模型的模型检查之间的联系，以便模型检查可以被编译器作者用作程序机械分析的首选工具。特别是，模型检查器使用的时态逻辑将被改编成用于编码数据流分析和基本安全属性的规范语言。其次，程序控制流分析的变种，即‘k-CFA’，将被发展成一种图形化的公式，它可以简单地从高阶的基于对象的程序和函数式程序中生成可检查的模型。(在通常情况下，这类程序没有可以机械检查的模型。)研究结果将影响编译器作者和软件工程师用来分析程序和验证程序的正确性和安全性的技术。

9970679 Schmidt, David A. Kansas State UniversityStatic Analysis Based on Model CheckingThis project aims toward integrating techniques based on temporal logic, program control-flow analysis, and data-flow analysis and applying the results to validating correctness and security properties of object-based and function-based programs. The work will proceed in two stages. First, the connection between program data-flow analysis and model checking of program models, uncovered by Steffen, will be developed and strengthened so that model checking can be used as the tool of choice by compiler writers for mechanical analysis of programs. In particular, the temporal logics used by model checkers will be adapted into specification languages for coding data-flow analyses and elementary security properties. Second, the variant of program control-flow analysis known as ``k-CFA'' will be developed into a graphical formulation that can simply generate checkable models from higher-order object-based and functional programs. (In the usual case, such programs do not have models that can be mechanically checked.) Results from the research will impact the techniques that compiler writers and software engineers use to analyze programs and validate the programs' correctness and security.