| Presentation | 2012-01-26 Automatic Generation of Non-linear Loop Invariants for Programs with Function Calls Eiichi SUZUKI, Toshiki SAKABE, Masahiko SAKAI, Keiichirou KUSAKARI, Naoki NISHIDA, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Finding loop invariants is one of the most important tasks in program verification. It is, however, difficult to automatically find meaningful loop invariants. In this report, we present a method for automatically generating loop invariants in the form of extended polynomial inequality, in which function instances may be included, over program variables. The method is based on the extended polynomial lemma which is improved to Farkas' Lemma. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | static analysis / program verification / invariant generation / weakest preconditon |
| Paper # | MSS2011-61,SS2011-46 |
| Date of Issue |
| Conference Information | |
| Committee | MSS |
|---|---|
| Conference Date | 2012/1/19(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Mathematical Systems Science and its applications(MSS) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Automatic Generation of Non-linear Loop Invariants for Programs with Function Calls |
| Sub Title (in English) | |
| Keyword(1) | static analysis |
| Keyword(2) | program verification |
| Keyword(3) | invariant generation |
| Keyword(4) | weakest preconditon |
| 1st Author's Name | Eiichi SUZUKI |
| 1st Author's Affiliation | Graduate School of Information Science, Nagoya University() |
| 2nd Author's Name | Toshiki SAKABE |
| 2nd Author's Affiliation | Graduate School of Information Science, Nagoya University |
| 3rd Author's Name | Masahiko SAKAI |
| 3rd Author's Affiliation | Graduate School of Information Science, Nagoya University |
| 4th Author's Name | Keiichirou KUSAKARI |
| 4th Author's Affiliation | Graduate School of Information Science, Nagoya University |
| 5th Author's Name | Naoki NISHIDA |
| 5th Author's Affiliation | Graduate School of Information Science, Nagoya University |
| Date | 2012-01-26 |
| Paper # | MSS2011-61,SS2011-46 |
| Volume (vol) | vol.111 |
| Number (no) | 405 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |