资源感知的程序逻辑理论及资源安全性推理

项目名称： 资源感知的程序逻辑理论及资源安全性推理

项目编号： No.61373033

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 秦胜潮

作者单位： 深圳大学

项目金额： 75万元

中文摘要： 计算机程序的运行离不开系统资源，如内存，CPU时间，能源供给等。合理、正确地使用这些系统资源是程序安全性和正确性的一个重要方面。错误或不合理的资源使用行为可能导致软件出错、系统崩溃，甚至可能危及人们的生命财产安全。因此，程序的资源安全性和正确性是软件安全可靠性的一个非常重要的方面。本项目的研究目标是构建对程序资源使用行为的自动分析与验证的基础理论以及资源安全性的推理技术。着重研究操作动态创建数据结构的程序的资源安全性和正确性，重点关注这类程序对系统资源使用和消耗的各种重要特性，并研究其理论模型和分析验证技术。本项目研究重点集中如下几个方面：在分离逻辑的基础上构建资源感知的规范描述语言；定义程序语言的资源感知语义； 搭建资源感知的程序验证逻辑框架和相应的推理机制；以及设计针对程序资源使用行为的静态分析算法。

中文关键词： 程序分析；软件验证；程序逻辑；程序理论；分离逻辑

英文摘要： System resources, such as memory space, power consumption and CPU computing time, have been a central concern in software systems. For example, in mobile and embedded systems, processes often compete for constrained CPU, memory and energy resources; effic

英文关键词： program analysis；software verification；program logic；program theories；separation logic