Invariants Synthesis over a Combined Domain for Automated Program Verification

Hdl Handle:
http://hdl.handle.net/10149/325648
Title:
Invariants Synthesis over a Combined Domain for Automated Program Verification
Other Titles:
Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday
Book Title:
Theories of Programming and Formal Methods
Authors:
Qin, S. (Shengchao); He, G. (Guanhua); Chin, W-N. (Wei-Ngan); Yang, H. (Hongli)
Editors:
Liu, Z. (Zhiming); Woodcock, J. (Jim); Zhu, H. (Huibiao)
Affiliation:
Teesside University. Digital Futures Institute
Citation:
Qin, S., He, G., Chin, W-N., Yang, H. (2013) 'Invariants Synthesis over a Combined Domain for Automated Program Verification' in Liu, Z., Woodcock, J., Zhu, H. Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday. Lecture Notes in Computer Science Volume 8051, 2013, pp 304-325
Publisher:
Springer Verlag
Issue Date:
2013
URI:
http://hdl.handle.net/10149/325648
DOI:
10.1007/978-3-642-39698-4_19
Additional Links:
http://link.springer.com/chapter/10.1007%2F978-3-642-39698-4_19
Abstract:
Program invariants such as loop invariants and method specifications ( a.k.a. procedural summaries) are key components in program verification. Such invariants are usually manually specified by users before passed as inputs to a program verifier. The process of manually annotating programs with such invariants is tedious and error-prone and can significantly hinder the level of automation in program verification. Although invariant synthesis techniques have made noticeable progress in reducing the burden of user annotations; when it comes to automated verification of memory safety and functional correctness for heap-manipulating programs, it remains a rather challenging task to discover program specifications and invariants automatically, due to the complexity of aliasing and mutability of data structures. In this paper, we present invariant synthesis algorithms for the following scenarios: i) to synthesise a missing loop invariant, ii) to refine given pre/post shape templates to complete pre/post-conditions, iii) to infer a missing precondition, iv) to calculate a missing postcondition, given a precondition. The proposed analyses are based on abstract interpretation and are built over an abstract domain combining separation, numerical and multi-set (bag) information. Our inference mechanisms are equipped with newly designed abstraction, join, widening and abduction operations. Initial prototypical experiments have shown that they are viable and powerful enough to discover interesting useful invariants 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.authorQin, S. (Shengchao)en
dc.contributor.authorHe, G. (Guanhua)en
dc.contributor.authorChin, W-N. (Wei-Ngan)en
dc.contributor.authorYang, H. (Hongli)en
dc.contributor.editorLiu, Z. (Zhiming)en
dc.contributor.editorWoodcock, J. (Jim)en
dc.contributor.editorZhu, H. (Huibiao)en
dc.date.accessioned2014-09-02T11:43:23Z-
dc.date.available2014-09-02T11:43:23Z-
dc.date.issued2013-
dc.identifier.doi10.1007/978-3-642-39698-4_19-
dc.identifier.urihttp://hdl.handle.net/10149/325648-
dc.description.abstractProgram invariants such as loop invariants and method specifications ( a.k.a. procedural summaries) are key components in program verification. Such invariants are usually manually specified by users before passed as inputs to a program verifier. The process of manually annotating programs with such invariants is tedious and error-prone and can significantly hinder the level of automation in program verification. Although invariant synthesis techniques have made noticeable progress in reducing the burden of user annotations; when it comes to automated verification of memory safety and functional correctness for heap-manipulating programs, it remains a rather challenging task to discover program specifications and invariants automatically, due to the complexity of aliasing and mutability of data structures. In this paper, we present invariant synthesis algorithms for the following scenarios: i) to synthesise a missing loop invariant, ii) to refine given pre/post shape templates to complete pre/post-conditions, iii) to infer a missing precondition, iv) to calculate a missing postcondition, given a precondition. The proposed analyses are based on abstract interpretation and are built over an abstract domain combining separation, numerical and multi-set (bag) information. Our inference mechanisms are equipped with newly designed abstraction, join, widening and abduction operations. Initial prototypical experiments have shown that they are viable and powerful enough to discover interesting useful invariants for non-trivial programs.en
dc.language.isoenen
dc.publisherSpringer Verlagen
dc.relation.urlhttp://link.springer.com/chapter/10.1007%2F978-3-642-39698-4_19en
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.titleInvariants Synthesis over a Combined Domain for Automated Program Verificationen
dc.title.alternativeEssays Dedicated to Jifeng He on the Occasion of His 70th Birthdayen
dc.typeBook Chapteren
dc.contributor.departmentTeesside University. Digital Futures Instituteen
dc.title.bookTheories of Programming and Formal Methodsen
or.citation.harvardQin, S., He, G., Chin, W-N., Yang, H. (2013) 'Invariants Synthesis over a Combined Domain for Automated Program Verification' in Liu, Z., Woodcock, J., Zhu, H. Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday. Lecture Notes in Computer Science Volume 8051, 2013, pp 304-325-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.