Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-39698-4_19
Title: Invariants synthesis over a combined domain for automated program verification
Authors: Qin, S.
He, G.
Chin, W.-N. 
Yang, H.
Issue Date: 2013
Source: Qin, S.,He, G.,Chin, W.-N.,Yang, H. (2013). Invariants synthesis over a combined domain for automated program verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 8051 LNCS : 304-325. ScholarBank@NUS Repository. https://doi.org/10.1007/978-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. © 2013 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/78201
ISBN: 9783642396977
ISSN: 03029743
DOI: 10.1007/978-3-642-39698-4_19
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

2
checked on Feb 21, 2018

Page view(s)

31
checked on Feb 17, 2018

Google ScholarTM

Check

Altmetric


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