Lenore Zuck: Witnessing: From Optimization to Verification to Optimization

Lunch: Please register in advance for lunch at  this doodle  or bring your own lunch.

*Abstract:*
An optimizing compiler is commonly structured as a sequence of passes each transforming a source program into a target one. The proof that a such a  transformation pass is correct consists of a relation between source and target, often with the aid of invariants.  Those invariants also enable further optimizations. Thus, the two tasks of proving the validity of a transformation and propagating invariants to enable further optimizations are closely related.  The two can be addressed by augmenting each transformation with A witness — a stuttering simulation relation between the target and source programs which guarantees correctness for that pass. This  stuttering simulation relation forms a sound and complete witness format.  Witnesses can be generated either automatically or by (sound) external static analyzers.

The talk will describe both witness generation and witness propagation, and demonstrate the feasibility of the approach on the LLVM compiler. Each optimization pass is augmented with a witness generator. This allows to construct an independent translation validation framework for the compiler as well as to generate an independent verification for each of its runs. The automatically generated invariants, as well as some obtained by Frama-C, can then propagated to enhance optimizations. This is demonstrated on experiments where  propagated witnesses are used to  substantially improve the effectiveness of several optimizations.

*Bio:* Lenore Zuck is Associate Professor at the University of Illinois, Chicago. Her research focuses on the applications of formal methods for analysis and verification of secure software systems. In particular, she is interested in the application of advanced theorem proving techniques to the area of security, privacy, optimizing compilers, and policy analysis. She is also interested in ethical and secure data sharing across borders.