Please use this identifier to cite or link to this item: https://doi.org/10.1016/j.scico.2013.03.004
Title: Automatically refining partial specifications for heap-manipulating programs
Authors: Qin, S.
He, G.
Luo, C.
Chin, W.-N. 
Yang, H.
Keywords: Constraint abstraction
Numerical analysis
Partial specification refinement
Semi-automatic software verification
Separation logic
Static program analysis
Issue Date: 3-Jan-2014
Citation: Qin, S., He, G., Luo, C., Chin, W.-N., Yang, H. (2014-01-03). Automatically refining partial specifications for heap-manipulating programs. Science of Computer Programming 82 : 56-76. ScholarBank@NUS Repository. https://doi.org/10.1016/j.scico.2013.03.004
Abstract: Automatically verifying heap-manipulating programs is a challenging task, especially when dealing with complex data structures with strong invariants, such as sorted lists and AVL/red-black trees. The verification process can greatly benefit from human assistance through specification annotations, but this process requires intellectual effort from users and is error-prone. In this paper, we propose a new approach to program verification that allows users to provide only partial specification to methods. Our approach will then refine the given annotation into a more complete specification by discovering missing constraints. The discovered constraints may involve both numerical and multi-set properties that could be later confirmed or revised by users. We further augment our approach by requiring partial specification to be given only for primary methods. Specifications for loops and auxiliary methods can then be systematically discovered by our augmented mechanism, with the help of information propagated from the primary methods. Our work is aimed at verifying beyond shape properties, with the eventual goal of analysing full functional properties for pointer-based data structures. Initial experiments have confirmed that we can automatically refine partial specifications with non-trivial constraints, thus making it easier for users to handle specifications with richer properties. © 2013 Elsevier B.V. All rights reserved.
Source Title: Science of Computer Programming
URI: http://scholarbank.nus.edu.sg/handle/10635/78037
ISSN: 01676423
DOI: 10.1016/j.scico.2013.03.004
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

6
checked on Nov 14, 2018

WEB OF SCIENCETM
Citations

4
checked on Oct 30, 2018

Page view(s)

76
checked on Nov 16, 2018

Google ScholarTM

Check

Altmetric


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