Name
Abstract | ||
|---|---|---|
A key problem in any automatic software verification system is the inference of loop invariants. When analyzing program structures involving disjunctive semantics, abstract interpretation has the problem of precision loss. Thus, some techniques were proposed to decompose such loop structures into a semantically equivalent sequence of loops with conjunctive semantics whose invariants can be generated by abstract interpretation directly. However, these works assumed that the iteration processes of nested branches are separate without consideration of non-monotone loop structures where those interweave with each other. In order to solve this problem, we present a novel static analysis technique for non-monotone loops. It analyzes loop convergence condition and traces the transfer between nested branches of finite non-monotone loops. With analytical results, it generates the loop invariants with precise semantics. Meanwhile, it takes advantage of cyclical nature of result expressions to restrict search space and accelerate computation procedure. Finally, experimental results show the potential of our approach, which is also helpful for reasoning about certain program security properties. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1109/COMPSAC.2018.00048 | 2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC) |
Keywords | Field | DocType |
invariant,static analysis,disjunctive semantics | Convergence (routing),Expression (mathematics),Abstract interpretation,Computer science,Static analysis,Algorithm,Real-time computing,Loop invariant,Invariant (mathematics),Monotone polygon,Software verification | Conference |
Volume | ISSN | ISBN |
01 | 0730-3157 | 978-1-5386-2667-2 |
Citations | PageRank | References |
0 | 0.34 | 3 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chunyan Hou | 1 | 11 | 6.09 |
| Jinsong Wang | 2 | 8 | 3.15 |
| Chen Chen | 3 | 9 | 3.18 |
| Kai Shi | 4 | 8 | 4.99 |