@article{oai:nagoya.repo.nii.ac.jp:00021410,
 author = {鈴木, 英一 and 坂部, 俊樹 and 酒井, 正彦 and 草刈, 圭一朗 and 西田, 直樹 and SUZUKI, Eiichi and SAKABE, Toshiki and SAKAI, Masahiko and KUSAKARI, Keiichirou and NISHIDA, Naoki},
 issue = {405},
 journal = {電子情報通信学会技術研究報告. MSS, システム数理と応用},
 month = {Jan},
 note = {プログラム検証において,ループ実行中に常に成り立つ論理式である不変式が重要な役割を持っている.しかし,検証に有効なループ不変式を自動的に発見することは一般には困難である.本稿では,プログラム変数と関数呼び出し項に関する非線形の不等式で表されるループ不変式を,線形計画法などで利用されるFarkasの補題を拡張した定理に基づいて自動生成する手法を示す., 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., IEICE Technical Report;MSS2011-61,IEICE Technical Report;SS2011-46},
 pages = {39--44},
 title = {関数呼び出しを持つプログラムの非線形ループ不変式の自動生成},
 volume = {111},
 year = {2012}
}