Survey Workshop on Corpus-based Shape Analysis

Overview

In this talk, we will introduce 4 papers which are related to our project, corpus-based shape analysis. In the papers, authors design and implement an automatic invariant generator for imperative programs. By using the information gathered from static abstract interpretation and dynamic execution of the program, the invariant generator can solve more scalable programs than classical means of program verification can. The approach of solving problems is similar to that of corpus-based shape analysis, and we expect that our approach will work well like the result of these papers.

Program

References

• M. Colon, S. Sankaranarayanan, and H. Sipma. “Linear invariant generation using non-linear constraint solving”. CAV'03.
• S. Sankaranarayanan, H. Sipma, and Z. Manna. “Scalable analysis of linear systems using mathematical programming”. VMCAI'05.
• S. Gulwani, S. Srivastava, and R. Venkatesan. “Program analysis as constraint solving”. PLDI'08.
• A. Gupta, R. Majumdar, and A. Rybalchenko. “From tests to proofs”. TACAS'09.
• S. Velupillai, M. Hassel, and H. Daliants. “Automatic dictionary construction and Identification of parallel text pairs”. In UCCTS, 2008.
• Michael Wilkinson. “Using specialized corpus to improve translation quality”. In Translation Journal, 2005
• Y. Muthusamy, R. Cole, and B. Oshika. “The OGI multi-language telephone speech corpus”. In ICSLP, 1992.
• G. Bugmann, E. Klein, S. Lauria, and T. Kyriacou. “Corpus-based robotics: A route instruction example”. In Intelligent autonomous systems 8, 2004.
• R. Mihalcea and H. Liu. “A corpus-based approach to finding happiness”. In AAAI, 2006.