Survey of Research on Program Verification via Separation Logic
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (61373033, 61502308, 61672358); Shenzhen Science and Technology Innovation Commission Project (JCYJ201418193546117)

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

    Since 1960s, automated program verification has been considered as an extremely difficult topic in Computer Science, despite of the emergence of Floyd-Hoare logic. Since 1990s, with more efforts and resources devoted to this area, especially the contributions from industry communities including Microsoft Research and IBM Research Centre, there has been noticeable progress made in program verification early this century. Two typical examples include ASTRÉE, used to verify the absence of runtime errors in Airbus code, and SLAM, employed to verify protocol properties of procedural calls in device drivers by Microsoft. However, none of these tools considers heap. Specifically, ASTRÉE assumes no dynamic pointer allocation and no recursion, while SLAM assumes memory safety. Many important programs/systems that exist nowadays, such as Linux, Apache, and device drivers, all make frequent use of heap. Automated verification of heap-manipulating programs remains a very challenging topic. The emergence of separation logic in 2001-2002 has shed some light into this area. With the key idea of separation and the elegant frame rule, local reasoning can now be readily employed in program verification. Since 2004, there have been a large body of research work dedicated to automated program verification via separation logic, e.g. SpaceInvader/Abductor, Slayer, HIP/SLEEK, CSL etc. This paper offers a survey on a number of important research work along this line.

    Reference
    Related
    Cited by
Get Citation

秦胜潮,许智武,明仲.基于分离逻辑的程序验证研究综述.软件学报,2017,28(8):2010-2025

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:November 25,2016
  • Revised:January 01,2017
  • Adopted:
  • Online: August 15,2017
  • Published:
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