Static Analysis Based on Model Checking

基于模型检验的静态分析

• 批准号: 9970679
• 负责人: David Schmidt
• 金额: $ 10.5万
• 依托单位: Kansas State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-09-01 至 2002-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9970679&HistoricalAwards=false
• 关键词: Static; Analysis; Based; Model; Checking

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.

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