ELŐADÁS
2014. december 22., hétfő, 11:00–12:00 óra
Tiberiu Popoviciu-terem (5/I), str. Mihail Kogălniceanu/ Farkas utca 1.

Termination and Non-Termination Reasoning with HIP/SLEEK

Előadó

Prof. dr. Wei-Ngan Chin
Department of Computer Science, National University of Singapore

Abstract

Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms. In this paper, we propose a novel mechanism that analyzes and proves both program termination and non-termination at the same time. We first introduce the concept of second-order termination constraints and accumulate a set of relational assumptions on them via a Hoare-style verification. We then solve these assumptions with case analysis to determine the (conditional) termination and non-termination scenarios expressed in some specification logic form. In contrast to current approaches, our technique can construct a summary of terminating and non-terminating behaviors for each method.

This enables modularity and reuse for our termination and non-termination proving processes. We have tested our tool on sample programs from a recent termination competition, and compared favorably against two state-of-the-art termination analyzer(s).

About the Speaker

Dr. Wei-Ngan Chin received his BSc and MSc in Computer Science from the University of Manchester and a PhD in Computing from Imperial College, London. He is presently an Associate Professor in the Department of Computer Science, National University of Singapore.

His research interests are in programming languages and software engineering. He has worked on various program analyses and verification techniques that are aimed at improving clarity, reliability and reusability of software. He and his students are currently building and enhancing an automated verification toolkit, called HIP/SLEEK, based on separation logic.