A Decidable Logic for Tree Data-Structures with Measurements

Speaker:        Professor Xiaokang Qiu
                Purdue University

Title:          "A Decidable Logic for Tree Data-Structures with
                 Measurements"

Date:           Monday, 29 May 2017

Time:           3:00pm - 4:00pm

Venue:          Room 5562 (via lifts 27/28), HKUST

Abstract:

We present a decidable logic that allows reasoning about tree
data-structures with measurements. This logic supports user-defined
recursive measurement functions such as height or size, and recursive
predicates such as AVL trees or red-black trees. We also show that this
logic is sufficient to express verification conditions for functional
correctness of recursive programs manipulating these data-structures. The
crux of the decidability proof is a small model property which allows us
to reduce the satisfiability of this logic to quantifier-free linear
arithmetic theory which can be solved efficiently using SMT solvers.
Experiments demonstrate that the decision procedure can effectively solve
formulas raised from natural proof verification and axioms describing
relationship between different tree measurements.


******************
Biography:

Xiaokang Qiu is an Assistant Professor of Electrical and Computer
Engineering at Purdue University. He finished his Ph.D. in Computer
Science at the University of Illinois at Urbana-Champaign in 2013. Before
starting at Purdue, he was a postdoctoral associate at the Massachusetts
Institute of Technology. He is interested in software verification and
synthesis, with a particular emphasis on heap-manipulating programs. His
research focuses on program logics, decision procedures, automated
verification, and syntax-guidedsynthesis. He is a member of the Purdue
Programming Languages (PurPL) research group and leads the Computer-Aided
Programming (CAP) group at Purdue.