Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-16901-4_31
Title: Loop invariant synthesis in a combined domain
Authors: Qin, S.
He, G.
Luo, C.
Chin, W.-N. 
Issue Date: 2010
Source: Qin, S.,He, G.,Luo, C.,Chin, W.-N. (2010). Loop invariant synthesis in a combined domain. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6447 LNCS : 468-484. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-16901-4_31
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, which can be tedious and error-prone and can significantly restrict the scalability of the verification system. In this paper, we reduce the need of user annotations by automatically inferring loop invariants over an abstract domain with both separation and numerical information. Our loop invariant synthesis is conducted automatically by a fixpoint iteration process, equipped with newly designed abstraction mechanism, and join and widening operators. Initial experiments have confirmed that we can synthesise loop invariants with non-trivial constraints. © 2010 Springer-Verlag Berlin Heidelberg.
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/41234
ISBN: 3642169007
ISSN: 03029743
DOI: 10.1007/978-3-642-16901-4_31
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

7
checked on Dec 11, 2017

Page view(s)

72
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


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