Structured Specification for Verification and Inference

Title: Structured Specification for Verification and Inference
Speaker: Wei-Ngan Chin (Department of Computer Science, National University of Singapore)
Time: 15:00, Tuesday, July 3rd, 2012
Venue: Lecture Room, 3rd Floor, Building 5#, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract:  Traditionally, the focus of specification mechanism has been on improving its ability to cover a wider range of problems more accurately, while the effectiveness of verification is left to the underlying theorem provers. Our work attempts a novel approach, where the focus is on designing good specification mechanisms to achieve better expressivity (the specification should capture more accurately and concisely the functionality of the corresponding code) and better verifiability (the verification process should succeed in more scenarios than the corresponding verification without the specification enhancements, with better or similar performance).

Moreover, we are also interested in providing the necessary tools to assist the user with the important but tedious task of constructing desired specifications. Existing approaches to specification construction tend to be either fully manual or fully automatic.

We propose a new framework for specification construction that can be done selectively and incrementally. This framework allows preconditions and postconditions to be selectively inferred via a set of specified variables, that included synthesis for unknown functions and relations.

Bio:
Chin Wei Ngan is an Associate Professor at the Dept of Computer Science, National University of Singapore. He has done extensive research on problem modelling based on advanced programming languages concepts, and have developed dependent type systems and specification logics that are aimed at constructing software systems with high levels of reliabity. Two of his recent projects were funded by ASTAR* and MoE Tier-2 grants. He currently leads a research group in programming language research with 7 PhD research students, and have been program chair APLAS04, ATVA10 and FTfJP12.