Automatically refining partial specifications for heap-manipulating programs

Hdl Handle:
http://hdl.handle.net/10149/325646
Title:
Automatically refining partial specifications for heap-manipulating programs
Authors:
Qin, S. (Shengchao); He, G. (Guanhua); Luo, C. (Chenguang); Chin, W. (Wei-Ngan); Yang, H. (Hongli)
Affiliation:
Teesside University. Digital Futures Institute
Citation:
Qin, S., He, G., Luo, C., Chin, W., Yang, H. (2014) 'Automatically refining partial specifications for heap-manipulating programs' Science of Computer Programming; 82:56
Publisher:
Elsevier
Journal:
Science of Computer Programming
Issue Date:
Mar-2014
URI:
http://hdl.handle.net/10149/325646
DOI:
10.1016/j.scico.2013.03.004
Additional Links:
http://linkinghub.elsevier.com/retrieve/pii/S0167642313000646
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.
Type:
Article
Language:
en
Keywords:
Static program analysis; separation logic; Numerical analysis; Partial specification refinement; Semi-automatic software verification; Constraint abstraction
ISSN:
01676423
Rights:
Author can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo [Accessed: 02/09/2014]

Full metadata record

DC FieldValue Language
dc.contributor.authorQin, S. (Shengchao)en
dc.contributor.authorHe, G. (Guanhua)en
dc.contributor.authorLuo, C. (Chenguang)en
dc.contributor.authorChin, W. (Wei-Ngan)en
dc.contributor.authorYang, H. (Hongli)en
dc.date.accessioned2014-09-02T11:38:39Z-
dc.date.available2014-09-02T11:38:39Z-
dc.date.issued2014-03-
dc.identifier.citationScience of Computer Programming; 82:56en
dc.identifier.issn01676423-
dc.identifier.doi10.1016/j.scico.2013.03.004-
dc.identifier.urihttp://hdl.handle.net/10149/325646-
dc.description.abstractAutomatically 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.en
dc.language.isoenen
dc.publisherElsevieren
dc.relation.urlhttp://linkinghub.elsevier.com/retrieve/pii/S0167642313000646en
dc.rightsAuthor can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo [Accessed: 02/09/2014]en
dc.subjectStatic program analysisen
dc.subjectseparation logicen
dc.subjectNumerical analysisen
dc.subjectPartial specification refinementen
dc.subjectSemi-automatic software verificationen
dc.subjectConstraint abstractionen
dc.titleAutomatically refining partial specifications for heap-manipulating programsen
dc.typeArticleen
dc.contributor.departmentTeesside University. Digital Futures Instituteen
dc.identifier.journalScience of Computer Programmingen
or.citation.harvardQin, S., He, G., Luo, C., Chin, W., Yang, H. (2014) 'Automatically refining partial specifications for heap-manipulating programs' Science of Computer Programming; 82:56-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.