Loop invariant synthesis in a combined abstract domain

Hdl Handle:
http://hdl.handle.net/10149/325647
Title:
Loop invariant synthesis in a combined abstract domain
Authors:
Qin, S. (Shengchao); He, G. (Guanhua); Luo, C. (Chenguang); Chin, W. (Wei-Ngan); Chen, X. (Xin)
Affiliation:
Teesside University. Digital Futures Institute
Citation:
Qin, S., He, G., Luo, C., Chin, W., Chen, X. (2013) 'Loop invariant synthesis in a combined abstract domain' Journal of Symbolic Computation; 50:386
Publisher:
Elsevier
Journal:
Journal of Symbolic Computation
Issue Date:
Mar-2013
URI:
http://hdl.handle.net/10149/325647
DOI:
10.1016/j.jsc.2012.08.007
Additional Links:
http://linkinghub.elsevier.com/retrieve/pii/S074771711200140X
Abstract:
Automated verification of memory safety and functional correctness for heap-manipulating programs has been a challenging task, especially when dealing with complex data structures with strong invariants involving both shape and numerical properties. Existing verification systems usually rely on users to supply annotations to guide the verification, which can be cumbersome and error-prone by hand and can significantly restrict the usability of the verification system. In this paper, we reduce the need for some user annotations by automatically inferring loop invariants over an abstract domain with both shape and numerical information. Our loop invariant synthesis is conducted automatically by a fixed-point iteration process, equipped with newly designed abstraction mechanism, together with join and widening operators over the combined domain. We have also proven the soundness and termination of our approach. Initial experiments confirm that we can synthesise loop invariants with non-trivial constraints.
Type:
Article
Language:
en
Keywords:
Loop invariant; Fixpoint analysis; Abstraction; Combining analysis; Shape analysis; Numerical analysis
ISSN:
07477171
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.authorChen, X. (Xin)en
dc.date.accessioned2014-09-02T11:41:28Z-
dc.date.available2014-09-02T11:41:28Z-
dc.date.issued2013-03-
dc.identifier.citationJournal of Symbolic Computation; 50:386en
dc.identifier.issn07477171-
dc.identifier.doi10.1016/j.jsc.2012.08.007-
dc.identifier.urihttp://hdl.handle.net/10149/325647-
dc.description.abstractAutomated verification of memory safety and functional correctness for heap-manipulating programs has been a challenging task, especially when dealing with complex data structures with strong invariants involving both shape and numerical properties. Existing verification systems usually rely on users to supply annotations to guide the verification, which can be cumbersome and error-prone by hand and can significantly restrict the usability of the verification system. In this paper, we reduce the need for some user annotations by automatically inferring loop invariants over an abstract domain with both shape and numerical information. Our loop invariant synthesis is conducted automatically by a fixed-point iteration process, equipped with newly designed abstraction mechanism, together with join and widening operators over the combined domain. We have also proven the soundness and termination of our approach. Initial experiments confirm that we can synthesise loop invariants with non-trivial constraints.en
dc.language.isoenen
dc.publisherElsevieren
dc.relation.urlhttp://linkinghub.elsevier.com/retrieve/pii/S074771711200140Xen
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.subjectLoop invarianten
dc.subjectFixpoint analysisen
dc.subjectAbstractionen
dc.subjectCombining analysisen
dc.subjectShape analysisen
dc.subjectNumerical analysisen
dc.titleLoop invariant synthesis in a combined abstract domainen
dc.typeArticleen
dc.contributor.departmentTeesside University. Digital Futures Instituteen
dc.identifier.journalJournal of Symbolic Computationen
or.citation.harvardQin, S., He, G., Luo, C., Chin, W., Chen, X. (2013) 'Loop invariant synthesis in a combined abstract domain' Journal of Symbolic Computation; 50:386-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.