本頁只刊出中文翻譯與中文說明；英文原文請見下方原文連結。
原文連結
論文資訊
- 類型：已發表論文
- 日期：2014-09-05
摘要
This article describes and evaluates DIG, a dynamic invariant generator that infers invariants from observed program traces, focusing on numerical and array variables. For numerical invariants, DIG supports both 非線性 equalities and inequalities of arbitrary degree defined over numerical program variables. For array invariants, DIG generates nested relations among multidimensional array variables. These properties are nontrivial and challenging for current static and dynamic invariant analysis methods. The key difference between DIG and existing dynamic methods is its generative technique, which infers invariants directly from traces, instead of using traces to filter out predefined templates. To generate accurate invariants, DIG employs ideas and tools from the 數學 and formal methods domains
※ 此為已發表論文，全文需透過期刊付費取得