University of Technology, Sydney

Staff directory | Webmail | Maps | Newsroom | What's on

QCIS Seminar: Optimisations Using Formally Verified Properties - Dr Yao Shi, UNSW, Australia

Presented by: Dr Yao Shi, NICTA & UNSW (invited by Prof Runyao Duan)

Abstract:  Formal program verification offers strong assurance of correctness, backed by the strength of mathematical proof.  Constructing these proofs requires humans to identify program invariants, and show that they are always maintained. These invariants are then used to prove that the code adheres to its specification. We explore the overlap between formal verification and code optimiSation. We propose two approaches to reuse the invariants derived in formal proofs and integrate them into a compilation.  The first applies invariants extracted from the proof, while the second leverages the property of program safety (ie. the absence of bugs).  We reuse this information to improve the performance of the generated object code. We evaluated these methods on seL4, a real-world, formally-verified micro-kernel, and obtained improvements in average runtime performance (up to 28%) and in worst-case execution time (up to 25%). In macro-benchmarks, we found the performance of para-virtualised Linux running on the micro-kernel improved by 6-16%.

Bio: Yao Shi received his PhD from Tsinghua University in 2010. He is a researcher at the National ICT Australia and a conjoint lecturer with the University of New South Wales. Yao is interested in operating systems, compiler optimisations, concurrent program analysis and software reliability. He was a developer of the Open64 compiler and has rich experience in the internals of mainstream compilers such as GCC and LLVM.

Selected publications: Code Optimizations Using Formally Verified Properties, Yao Shi, Bernard Blackham, Gernot Heisor, OOPSLA'13; Improving Interrupt Response Time in a Verifiable Protected Microkernel, Bernard Blackham, Yao Shi and Gernot Heiser, Eurosys'12; Timing Analysis of a Protected Operating System Kernel, Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser, RTSS'11; Protected Hard Real-Time: The Next Frontier, Bernard Blackham, Yao Shi and Gernot Heiser, Apsys'11; Do I Use the Wrong Definition? DefUse: Definition-Use Invariants for Detecting Concurrency and Sequential Bugs, Yao Shi, Soyeon Park, Zuoning Yin, Shan Lu, Yuanyuan Zhou, Wenguang Chen and Weimin Zheng, OOPSLA'10.


21 August 2013
14:00 - 15:30
City - Broadway CB02 Level 4, Room 10
All Welcome
Barbara Munday

Back to list of Past Events