微信服务号

微信订阅号

2025-4-24- 11
Home > Archive>Volume 27, Issue 7, 2016 >1741-1756. DOI:10.13328/j.cnki.jos.004836
PDF HTML XML Export Cite reminder
Improving Invariant Generation for Loops Containing Disjunctive Semantics
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61170070, 61572248, 61431008, 61321491); National Key Technology Research and Development Program of the Ministry of Science and Technology of China (2012BAK26B01); National High Technology Research and Development Program of China (863) (2011AA1A202)

  • Article
    • | |
  • Metrics
    • |
  • Reference
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    Abstract interpretation provides a general framework to generate program invariants automatically. However, most existing numerical abstract domains under this framework can only express constraint sets that are geometrically convex. Therefore, using convex abstract domains to analyze special program structures involving disjunctive semantics (whose constraint sets are non-convex) may lead to imprecise results. This paper presents a novel approach based on loop decomposition and deduction to improve invariant generation for loop structures with explicit and implicit disjunctive semantics. This approach can alleviate the problem of great semantic loss during abstract interpretation of loop structures with disjunctive semantics. Compared with existing approaches, experimental results show that the presented approach can generate more precise invariants for loop structures involving disjunctive semantics, which is also helpful for reasoning about certain security properties.

    Reference
    Related
    Cited by
Get Citation

潘建东,陈立前,黄达明,孙浩,曾庆凯.含有析取语义循环的不变式生成改进方法.软件学报,2016,27(7):1741-1756

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:December 12,2014
  • Revised:March 02,2015
  • Online: November 12,2015
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063