Invited talk: Program Verification for Data Structures, Higher-Order Functions and Beyond

Speaker: Wei-Ngan Chin, National University of Singapore

Ph.D. (Computing, Imperial College of Science, Technology and Medicine)

M.Sc. (Computer Science, University of Manchester)

B.Sc. (Computer Science, Honours I, University of Manchester)

RESEARCH INTERESTS

  • Advanced Type Systems
  • Program Analysis and Optimization
  • Dependable Software
  • Verification

https://www.comp.nus.edu.sg/cs/people/chinwn/

 At Faculty of Automatic Control and Computers – September 15, 2025, 13:00, Room ED 109

Professor Wei-Ngan Chin is a faculty member of the School of Computing at the National University of Singapore. He received his BSc and MSc in Computer Science from the University of Manchester and his PhD in Computing at Imperial College London.

Professor Chin’s research focuses on programming languages and software engineering, particularly automated verification via separation logic, automated specification discovery for trusted software, dependable software construction, and type-based analyses.

He has made significant contributions to program analysis and verification techniques aimed at improving the clarity, reliability, and reusability of software.

He has published more than 250 papers in leading international conferences and journals.

Speaker: Wei-Ngan Chin, National University of Singapore

Title: Program Verification for Data Structures, Higher-Order Functions and Beyond

Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification and reasoning, due to the use of yet-to-be-instantiated function parameters. One inherent limitation of existing specification mechanisms is its reliance on only two stages: an initial stage to denote the precondition at the start of the method and a final stage to capture the postcondition. Such two-stage specifications force abstract properties to be imposed on unknown function parameters, leading to less precise specifications for higher-order methods.

In this talk, we discuss the challenges of automated program verification, starting with data structures, first-order functions and while-loops; and then making steady progression to imperative higher-order programs via a new logic, called staged logics. We show how this new logic (with multiple stages) can be used to support reasoning with a recent language construct, that relies on delimited continuations, known as algebraic effects.