Abstract
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.
Short bio
Deepak Kapur is a distinguished professor of computer science at
University of New Mexico, USA. From 1998 until 2006, he served as
the 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 as
on 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 the
Herbrand Award for distinguished contributions to automated reasoning.
Resources
This will be shown to users with no Flash or Javascript.
|
