中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
Subject: 计算机科学技术基础学科
Title:
基于公式学习的循环不变式的推导
Author: 哈晓琳
Issued Date: 2014-05-28
Supervisor: 李勇坚
Major: 计算机软件与理论
Degree Grantor: 中国科学院研究生院
Place of Degree Grantor: 北京
Degree Level: 硕士
Keyword: 循环不变式 ; CDNF ; 机器学习 ; 布尔公式学习算法 ; 形式验证
Abstract:
随着因特网的发展和计算机的普及,软硬件的发展给人们提供了各种便利高效的手段。“软件危机”出现以来,软件的正确性是人们非常重视的一个问题,计算机领域的科学家们也对如何正确的开发和验证软件进行了一系列研
究,其中,软件的形式化验证被称为解决“软件危机”的重要手段。
针对程序的形式化验证,当前主要是基于霍尔逻辑方面的研究。对于形式化验证中最复杂的问题–循环不变式的生成,已经有众多科学家提出了多种解决方法。本文主要针对近年来新提出的基于公式学习的循环不变式的推导方法进行了研究:
1. 对程序的形式化验证中重要的基本理论进行系统性的总结。本文介绍了结构化程序的形式验证的重要基础:公理语义和霍尔理论。并对循环不变式的重要意义进行了分析总结。
2. 分析研究了基于公式学习的循环不变式推导算法的核心–布尔公式学习算法,提出了根据最小赋值向量改进公式学习算法的思路,证明了可行性的相关理论,并提出根据改进思路设计的两种改进算法,对改进的算法和原始算法进行了程序实现和实验。验证了改进算法的正确性和高效性,并分析总结了布尔公式学习算法效率方面主要影响因素,以及改进的算法的可扩展性。
3. 分析总结了基于公式学习的循环不变式推导算法的整体框架。对于其中使用的谓词抽象技术,静态分析技术和SMT求解技术进行了研究和总结,并对算法中对于各个部分的联接和转换进行了深度剖析。
4. 提出了自己改进的布尔公式学习算法在循环不变式推导中应该如何应用的设计方案,详细分析了方案的可行性,设计了改进的算法需要用到的工具和方法,验证了改进的布尔公式学习算法的高可移植性。并且,分析了基于公式学习的循环不变式推导算法的优缺点。
English Abstract:
With the universal of the Internet and the proliferation of computers, the development of hardware and software provide people with a variety of convenient and efficient means. Since the emergence of ”Software crisis”, program correctness is an issue that people take very seriously. The scientists also study how to properly develop and validate software. Among a series of studies, the formal verification of software is known as an important mean to solve the ”software crisis”.
In the formal verification, the current study is mainly based on the Hoare logic. One of the most complex problem in formal verification is loop invariant generation. Many scientists have proposed a variety of solutions to solve it. This paper mainly studies the formula learning based approach in loop invariant derivation, which was a relatively new idea in recent years.
1. Give a systematic summary of the important basic theory of the formal verification. This article describes the important basis for structured programs’verification, which are axiomatic semantics and Hoare logic, as well as the significance and analyse of the loop invariant.
2. Analysis of the core algorithm in the formula learning based derivation of loop invariant,which is the boolean function learning algorithm CDNF.Propose two improved boolean function learning algorithm using minterm theory, and implement the new two algorithms and the original algorithm. We use the abstracted loop invariants to experiment them, and analyse the impact factors to the boolean function learning algorithm. And what’s more, we verify the correctness and higher efficiency of the improved algorithm.
3. Summarize the frame of the function learning based loop invariant derivation algorithm. Describe predicate abstraction techniques, static analysis technology and SMT solving techniques,which were used in the frame. And analyse the algorithm for converting various parts of the joints.
4. Put forward our own learning algorithm using improved boolean function learning algorithm in the loop invariant derivation. we describe how to apply the design in detail, analysis of the feasibility and design tools and methods needed in the improve the algorithm. Lastly ,we verify high portability of the improved boolean function learning algorithm.And analyze the advantages and disadvantages of algorithmic learning based invariant derivation.
Language: 中文
Content Type: 学位论文
URI: http://ir.iscas.ac.cn/handle/311060/16488
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
基于公式学习的循环不变式的推导.pdf(2488KB)----限制开放 联系获取全文

Recommended Citation:
哈晓琳. 基于公式学习的循环不变式的推导[D]. 北京. 中国科学院研究生院. 2014-05-28.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[哈晓琳]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[哈晓琳]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace