Loop Invariant Synthesis in a Combined Domain

Shengchao Qin; Guanhua He; Chenguang Luo; Wei-Ngan Chin

doi:10.1007/978-3-642-16901-4_31

Loop Invariant Synthesis in a Combined Domain

Shengchao Qin, Guanhua He, Chenguang Luo, Wei-Ngan Chin

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings
Publisher	Springer Berlin
Pages	468-484
ISBN (Electronic)	9783642169014
ISBN (Print)	9783642169007
DOIs	https://doi.org/10.1007/978-3-642-16901-4_31
Publication status	Published - 2010
Event	Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods - Shanghai, China Duration: 17 Nov 2010 → 19 Nov 2010 Conference number: 12

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer

Conference

Conference	Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods
Abbreviated title	ICFEM 2010
Country/Territory	China
City	Shanghai
Period	17/11/10 → 19/11/10

Access to Document

10.1007/978-3-642-16901-4_31

Cite this

Qin, S., He, G., Luo, C., & Chin, W.-N. (2010). Loop Invariant Synthesis in a Combined Domain. In Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings (pp. 468-484). (Lecture Notes in Computer Science ). Springer Berlin. https://doi.org/10.1007/978-3-642-16901-4_31

@inproceedings{2e611f12ebbe4ea7b596b203973def20,

title = "Loop Invariant Synthesis in a Combined Domain",

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.",

author = "Shengchao Qin and Guanhua He and Chenguang Luo and Wei-Ngan Chin",

year = "2010",

doi = "10.1007/978-3-642-16901-4_31",

language = "English",

isbn = "9783642169007",

series = "Lecture Notes in Computer Science ",

publisher = "Springer Berlin",

pages = "468--484",

booktitle = "Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings",

address = "Germany",

note = "Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010 ; Conference date: 17-11-2010 Through 19-11-2010",

}

Qin, S, He, G, Luo, C & Chin, W-N 2010, Loop Invariant Synthesis in a Combined Domain. in Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings. Lecture Notes in Computer Science , Springer Berlin, pp. 468-484, Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, Shanghai, China, 17/11/10. https://doi.org/10.1007/978-3-642-16901-4_31

Loop Invariant Synthesis in a Combined Domain. / Qin, Shengchao; He, Guanhua; Luo, Chenguang et al.
Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings. Springer Berlin, 2010. p. 468-484 (Lecture Notes in Computer Science ).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Loop Invariant Synthesis in a Combined Domain

AU - Qin, Shengchao

AU - He, Guanhua

AU - Luo, Chenguang

AU - Chin, Wei-Ngan

N1 - Conference code: 12

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

UR - http://dx.doi.org/10.1007/978-3-642-16901-4_31

U2 - 10.1007/978-3-642-16901-4_31

DO - 10.1007/978-3-642-16901-4_31

M3 - Conference contribution

SN - 9783642169007

T3 - Lecture Notes in Computer Science

SP - 468

EP - 484

BT - Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings

PB - Springer Berlin

T2 - Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods

Y2 - 17 November 2010 through 19 November 2010

ER -

Loop Invariant Synthesis in a Combined Domain

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this