[pl-seminar] PL Seminar / Practice Job Talk (TODAY at 4 pm)

[Alexey Loginov <alexey@xxxxxxxxxxx>]

PRESENTER: Alexey Loginov
TITLE:     Program Verification via Three-Valued Logic Analysis
WHERE:     CS 2310
WHEN:      4 pm today (Tuesday, 3/14)
WHY:       I need your input; you need cookies

Dear all,

I would like to get your input on my job talk today.  Input from PL
folks, as well as those outside the area would be greatly
appreciated.  To avoid keeping you too long after 5, I plan to start
promptly at 4 pm.

Thank you very much!
-Alexey


Title: Program Verification via Three-Valued Logic Analysis

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.