Please use this identifier to cite or link to this item: https://doi.org/10.1016/j.jsc.2012.08.007
Title: Loop invariant synthesis in a combined abstract domain
Authors: Qin, S.
He, G.
Luo, C.
Chin, W.-N. 
Chen, X.
Keywords: Abstraction
Combining analysis
Fixpoint analysis
Loop invariant
Numerical analysis
Separation logic
Shape analysis
Issue Date: 2013
Source: Qin, S., He, G., Luo, C., Chin, W.-N., Chen, X. (2013). Loop invariant synthesis in a combined abstract domain. Journal of Symbolic Computation 50 : 386-408. ScholarBank@NUS Repository. https://doi.org/10.1016/j.jsc.2012.08.007
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. © 2012 Elsevier B.V.
Source Title: Journal of Symbolic Computation
URI: http://scholarbank.nus.edu.sg/handle/10635/39613
ISSN: 07477171
DOI: 10.1016/j.jsc.2012.08.007
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

11
checked on Dec 5, 2017

WEB OF SCIENCETM
Citations

6
checked on Dec 5, 2017

Page view(s)

81
checked on Dec 11, 2017

Google ScholarTM

Check

Altmetric


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