Loop invariants play a central role in ensuring the reliability of software. Program analysis techniques must either require such program annotations at appropriate program locations or automatically derive these annotations from a program. A new approach for automatically generating loop invariants from imperative programs will be presented. Loop invariants are assumed to have certain shape, i.e., they are formulas in a restricted quantifier-free first-order theory. Elimination techniques can be used to generate such invariants. The focus of this talk will be on exploring heuristics for quantifier-elimination so that such techniques can scale well. A nice feature of the proposed approach is that it does not need to have access to any specification or annotations associated with a program. Some preliminary ideas about how to generalize these approaches to work on data types other than numbers will be discussed.

Deepak Kapur is a distinguished professor of computer science at University of New Mexico, USA. From 1998 until 2006, he served asthe chair of the computer science department there. He got his Ph.D. in computer science in 1980 from MIT, and B.Tech and M. Tech from IIT, Kanpur, India, in 1971, and 1973 respectively. After his Ph.D., he worked at the GE R&D Center in Schenectady, USA. In 1988, he was hired as a full tenured professor by the State University of New York, Albany, USA. He has held visiting positions at MIT, Max Planck Institute, IBM Research, TIFR, and IIT. He has conducted research in areas of automated deduction, induction theorem proving, term rewriting, unification theory, formal methods, program analysis, hardware verification, algebraic and geometric reasoning and their applications. His group built one of the first rewrite-based theorem provers, called Rewrite Rule Laboratory. He served as the editor-in-chief of the Journal of Automated Reasoning from 1993-2007. He is on the editorial board of many journals including Journal of Symbolic Computation, as well ason the editorial board of the new open access initiative LIPIcs started in cooperation with Schloss Dagstuhl-Leibniz Center. He also serves on the Board of Directors of theUnited Nations University's International Institute for Software Technology, Macau. In 2009, he received theHerbrand Award for distinguished contributions to automated reasoning.

Contact: Kwangkeun Yi(이광근 교수), x1857(02 880 1857)

Deepak Kapur is a distinguished professor of computer science at University of New Mexico, USA. From 1998 until 2006, he served asthe chair of the computer science department there. He got his Ph.D. in computer science in 1980 from MIT, and B.Tech and M. Tech from IIT, Kanpur, India, in 1971, and 1973 respectively. After his Ph.D., he worked at the GE R&D Center in Schenectady, USA. In 1988, he was hired as a full tenured professor by the State University of New York, Albany, USA. He has held visiting positions at MIT, Max Planck Institute, IBM Research, TIFR, and IIT. He has conducted research in areas of automated deduction, induction theorem proving, term rewriting, unification theory, formal methods, program analysis, hardware verification, algebraic and geometric reasoning and their applications. His group built one of the first rewrite-based theorem provers, called Rewrite Rule Laboratory. He served as the editor-in-chief of the Journal of Automated Reasoning from 1993-2007. He is on the editorial board of many journals including Journal of Symbolic Computation, as well ason the editorial board of the new open access initiative LIPIcs started in cooperation with Schloss Dagstuhl-Leibniz Center. He also serves on the Board of Directors of theUnited Nations University's International Institute for Software Technology, Macau. In 2009, he received theHerbrand Award for distinguished contributions to automated reasoning.

Contact: Kwangkeun Yi(이광근 교수), x1857(02 880 1857)