Title:AutomaticVerificationTechniquesforHeap-ManipulatingPrograms

Abstract: Reliability is critical for system software such as OS kernels and mobile
browsers, as well as applications such as office software and mail clients. The
functional correctness of these programs is highly desirable, as they should provide
a trustworthy platform for higher- level applications. Unfortunately, due to its
inherent complexity, the verification process of these programs is typically
manual/semi-automatic, and painful. It usually eludes all existing automatic techniques and tools,
and poses one of the greatest challenges in software verification.

In this talk, I will present two logic-based automatic software verification systems,
namely Strand and Dryad. Strand is a logic that combines an expressive heap-logic with
an arbitrary data-logic and admits several powerful decidable fragments. The decision
procedures can be used in not only proving programs correct but also in software analysis
and testing. Dryad is a dialect of separation logic that is amenable to automated reasoning
using the natural proof strategy. Dryad is so far the only logic that can verify the full
correctness of a wide variety of challenging programs, including a large number of C programs
from various open-source libraries. I will also present an ongoing project on encoding the
 natural proof strategy in ghost annotations in VCC. The aim is to prove C programs automatically
using the natural proof techniques, without extra burden for the programmer.

Bio: Xiaokang Qiu is a Ph.D. candidate in the Department of Computer Science at the University
of Illinois at Urbana-Champaign. He received his B.S. degree and M.Eng. degree from Nanjing
University, both in Computer Science. His research interests are in the area of program analysis and
verification, with particular emphasis on algorithmic verification of functional program
correctness. His recent work includes logic-based automatic verification systems for heap-manipulating
 programs. Papers based on his thesis work have been or to be published on several premier
 conferences, such as POPL'11, POPL'12 and PLDI'13.