The Colloquium Series of the
            Department of Computer Science,
		  University of Wyoming

			presents

                   Dr. Alexey Loginov
             University of Wisconsin-Madison

  "Program Verification via Three-Valued Logic Analysis"

                 Monday, March 20, 2006
                        ENG 4066
                     4:00 - 5:00 p.m.


Abstract:

Software errors cost the US economy billions of dollars each year.
According to reasonable estimates, a third of the cost can be saved
through the use of enhanced tools for software quality.  My dissertation
addresses a key challenge in software verification: how to analyze
programs that perform destructive manipulation of linked (or recursive)
data structures.  I applied the concept of abstraction refinement to the
problem of automating shape analysis, static analysis that establishes
properties of such programs.  My thesis exposed a new connection between
Machine Learning and program analysis--in particular, that Inductive
Logic Programming (ILP) provides a key primitive for abstraction
refinement.  The techniques developed in my thesis have been implemented
as extensions to the Three-Valued Logic Analysis tool, or TVLA.  They
allowed the automatic verification of a number of interesting properties
of programs that destructively manipulate singly- and doubly-linked
lists, binary trees, and binary-search trees.