Name
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. |
Year | Venue | Keywords |
|---|---|---|
2010 | ICFEM | abstract domain,strong invariants,existing verification system,verification system,numerical property,inferring loop invariants,automated verification,combined domain,loop invariants,loop invariant synthesis,numerical information,memory safety,complex data |
Field | DocType | Volume |
Memory safety,Computer science,Invariant (computer science),Correctness,Algorithm,Theoretical computer science,Loop invariant,Symbolic execution,Invariant (mathematics),High-level verification,Scalability | Conference | 6447 |
ISSN | ISBN | Citations |
0302-9743 | 3-642-16900-7 | 7 |
PageRank | References | Authors |
0.44 | 23 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shengchao Qin | 1 | 711 | 62.81 |
| Guanhua He | 2 | 68 | 7.50 |
| Chenguang Luo | 3 | 56 | 5.63 |
| Wei-Ngan Chin | 4 | 868 | 63.37 |