Automatic Program Verification using Separation Logic
A series of lectures by Prof. Chin Wei Ngan (National University of Singapore)
VERIMAG Historic Building, Salle Turing
Lecture 1: Friday December 12 between 10:00-12:00 and 14:00-16:00
Automated Verification with HIP/SLEEK
Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In recent years, separation logic has emerged as a contender for formal reasoning of pointer-based programs. Recent works have focused on specialized provers that are mostly based on fixed sets of predicates. In this talk, we propose an automated verification system for ensuring the safety of pointer-based programs, where specifications handled are con- cise, precise and expressive. Our approach uses user-definable predicates to allow programmers to describe a wide range of data structures with their associated shape, size and bag (multi-set) properties. To support automatic verification, we design a new entailment checking procedure, called SLEEK, which can handle inductively defined predicates by using unfold/fold reasoning together with proof search via lemma. We have also built a program verifier, called HIP, on top of SLEEK. To support automated verification, we have also designed an expressive structured specification mechanisms, in conjunction with a logic which naturally captures exceptions. Our approach supports proof-search and is able to structured to support automatic case-analysis. In addition, we have designed proof slicing mechanism to allow more scalable automated verification to be attained.
Lecture 2: Tuesday December 16 between 10:00-12:00 and 14:00-16:00
From Verification to Specification Inference
Traditionally, one could either perform automated verification when given some specification, or directly perform analysis on programs to recover their specification. In this talk, we show how one may transition from verification to specification inference by controlling pres-state we may allow to be inferred. This concept was first pioneered in bi-abduction but we made two major improvements (i) selective inference (ii) second-order unknowns. We show how entailment procedure can be generalized to support selective inference. We also show how shape analysis and pure analysis can be crafted into such a specification inference framework. As a middle ground, we show how partial specification can be both verified and inferred, allowing users and systems to play complementary roles in program specification and automated verification.
Lecture 3: Thursday December 18 between 10:00-12:00 and 14:00-16:00
Termination and Non-Termination Reasoning with HIP/SLEEK
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 %% (unknown) 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).
