Program Verification via Three-Valued Logic Analysis

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.

Speaker Details

Alexey Loginov was born and raised in St. Petersburg, Russia. In 1994 Alexey obtained his undergraduate degrees in Mathematics and Computer Science at the University of Texas at Austin. He spent the next three years as a software engineer at Hewlett-Packard Company in San Diego. In 1999 he obtained his Master’s degree in Computer Science at the University of Wisconsin at Madison. After spending the academic year of 2000-2001 working on datarace detection for multithreaded Java applications with Drs. Jong-Deok Choi and Vivek Sarkar at IBM T.J. Watson Research Center, Alexey returned to Wisconsin, where he started his work on program verification via Three-Valued Logic Analysis under the supervision of Dr. Thomas Reps.Alexey’s primary research interests lie in program analysis for program verification, program understanding, debugging, and reverse engineering. He is interested in interdisciplinary approaches to software quality–in particular, the use of Machine Learning for program analysis.

Date:
Speakers:
Alexey Loginov
Affiliation:
University of Wisconsin at Madison

    • Portrait of Jeff Running

      Jeff Running