View source for Automatic Program Verification using Separation Logic



				
== Automatic Program Verification via Separation Logic ==
 
				

				A series of lectures by Prof. Chin Wei Ngan 
				  (National University of Singapore)

				  VERIMAG Historic Building, Salle Turing
				  http://www-verimag.imag.fr/Venir-a-Verimag.html?lang=


Lecture 1: Friday December 12 between 10:00-12:00 and 14:00-16:00 

* [http://loris-7.ddns.comp.nus.edu.sg/~project/Tut1/index.html Tutorial 1 : Automated Verification]

'''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).