Pat Hill - Proving Properties of Logic Programs

Abstract interpretation theory has successfully been used for constructing algorithms to statically determine run-time properties of programs. The central notion is to approximate the program's semantics by defining an abstract domain with operations which mimic those of the concrete domain. Its application to logic programming has been particularly productive as LP has such a well-defined semantics, both from the declarative and from the procedural perspectives. Central to AI is the notion of an abstract domain, describing certain program properties. However, most domains that simply represent an interesting property are rather imprecise as, normally, too much information is lost in the abstract interpretation of the program. Thus, there is an art in finding good domains that provide accurate information within an acceptable period of time and memory. How such domains can be constructed, combined and refined is the main topic of this talk.