Automated Specification Discovery via User-Defined Predicates

Hdl Handle:
http://hdl.handle.net/10149/325632
Title:
Automated Specification Discovery via User-Defined Predicates
Book Title:
Formal Methods and Software Engineering
Authors:
He, G. (Guanhua); Qin, S. (Shengchao); Chin, W-N. (Wei-Ngan); Craciun, F. (Florin)
Editors:
Groves, L. (Lindsay); Sun, J. (Jing)
Affiliation:
Teesside University. Digital Futures Institute
Citation:
He, G., Qin, S., Chin, W-N., Craciun, F. (2013) 'Automated Specification Discovery via User-Defined Predicates' in Groves, L., Sun, J. Formal Methods and Software Engineering; Lecture Notes in Computer Science Volume 8144, 2013, pp 397-414
Publisher:
Springer Verlag
Issue Date:
2013
URI:
http://hdl.handle.net/10149/325632
DOI:
10.1007/978-3-642-41202-8_26
Additional Links:
http://link.springer.com/chapter/10.1007%2F978-3-642-41202-8_26
Abstract:
Automated discovery of specifications for heap-manipulating programs is a challenging task due to the complexity of aliasing and mutability of data structures. This task is further complicated by an expressive domain that combines shape, numerical and bag information. In this paper, we propose a compositional analysis framework in the presence of user-defined predicates, which would derive the summary for each method in the expressive abstract domain, independently from its callers. We propose a novel abstraction method with a bi-abduction technique in the combined domain to discover pre-/post-conditions that could not be automatically inferred before. The analysis does not only prove the memory safety properties, but also finds relationships between pure and shape domains towards full functional correctness of programs. A prototype of the framework has been implemented and initial experiments have shown that our approach can discover interesting properties for non-trivial programs.
Type:
Book Chapter
Language:
en
Rights:
SUbject to 12 month embargo 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.authorHe, G. (Guanhua)en
dc.contributor.authorQin, S. (Shengchao)en
dc.contributor.authorChin, W-N. (Wei-Ngan)en
dc.contributor.authorCraciun, F. (Florin)en
dc.contributor.editorGroves, L. (Lindsay)en
dc.contributor.editorSun, J. (Jing)en
dc.date.accessioned2014-09-02T11:32:21Z-
dc.date.available2014-09-02T11:32:21Z-
dc.date.issued2013-
dc.identifier.doi10.1007/978-3-642-41202-8_26-
dc.identifier.urihttp://hdl.handle.net/10149/325632-
dc.description.abstractAutomated discovery of specifications for heap-manipulating programs is a challenging task due to the complexity of aliasing and mutability of data structures. This task is further complicated by an expressive domain that combines shape, numerical and bag information. In this paper, we propose a compositional analysis framework in the presence of user-defined predicates, which would derive the summary for each method in the expressive abstract domain, independently from its callers. We propose a novel abstraction method with a bi-abduction technique in the combined domain to discover pre-/post-conditions that could not be automatically inferred before. The analysis does not only prove the memory safety properties, but also finds relationships between pure and shape domains towards full functional correctness of programs. A prototype of the framework has been implemented and initial experiments have shown that our approach can discover interesting properties for non-trivial programs.en
dc.language.isoenen
dc.publisherSpringer Verlagen
dc.relation.urlhttp://link.springer.com/chapter/10.1007%2F978-3-642-41202-8_26en
dc.rightsSUbject to 12 month embargo author 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.titleAutomated Specification Discovery via User-Defined Predicatesen
dc.typeBook Chapteren
dc.contributor.departmentTeesside University. Digital Futures Instituteen
dc.title.bookFormal Methods and Software Engineeringen
or.citation.harvardHe, G., Qin, S., Chin, W-N., Craciun, F. (2013) 'Automated Specification Discovery via User-Defined Predicates' in Groves, L., Sun, J. Formal Methods and Software Engineering; Lecture Notes in Computer Science Volume 8144, 2013, pp 397-414-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.