跳到主要导航 跳到搜索 跳到主要内容

Automated program verification using generation of invariants

  • Jianying Xing*
  • , Mengjun Li
  • , Zhoujun Li
  • *此作品的通讯作者
  • National University of Defense Technology

科研成果: 书/报告/会议事项章节会议稿件同行评审

摘要

Program verification based on invariant generation is a central issue in recent years. Invariants are key to deductive verification of imperative programs. In this paper, depending on linear invariants and polynomial loop invariants, we present a practical program verification framework. The safety property and the termination property can be verified automatically. The experimental results demonstrate the power of our approach.

源语言英语
主期刊名Proceedings - 10th International Conference on Quality Software, QSIC 2010
300-305
页数6
DOI
出版状态已出版 - 2010
活动10th International Conference on Quality Software, QSIC 2010 - Zhangjiajie, 中国
期限: 14 7月 201015 7月 2010

出版系列

姓名Proceedings - International Conference on Quality Software
ISSN(印刷版)1550-6002

会议

会议10th International Conference on Quality Software, QSIC 2010
国家/地区中国
Zhangjiajie
时期14/07/1015/07/10

指纹

探究 'Automated program verification using generation of invariants' 的科研主题。它们共同构成独一无二的指纹。

引用此