Benchmark Suites

• NLA: Programs consisting of nonlinear polynomial invariants from DIG papers
• Mccune: Programs with Octagonal invariants from Mccune paper.

Papers

• Deepak Kapur, Zhihai Zhang, Matthias Horbach, Hengjun Zhao, Qi Lu, and ThanhVu Nguyen. Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants. In Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, volume 7788, pages 189--228. Springer, 2013.

• ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. Transactions on Software Engineering Methodology (TOSEM), 23(4):30:1--30:30, 2014. [ bib | Code | Paper | Abstract ]

• ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. Using Dynamic Analysis to Generate Disjunctive Invariants. In International Conference on Software Engineering (ICSE), pages 608--619. IEEE, 2014. [ bib | Code | Slides | Paper | Abstract ]