Output details
11 - Computer Science and Informatics
Queen Mary University of London
Compositional Shape Analysis by Means of Bi-Abduction
<11>This paper is the first to take automatic program shape analysis to millions of lines of code. The new approach is based on abductive inference, a technique not previously used in program verification, but that, following this paper, is becoming widely used. Besides being influential in the research community, our approach forms the basis of Monoidics Ltd's technology (customers include Airbus, Arm, Mitsubishi), recently sold to Facebook. This paper led to the 2012 Needham Award and keynote addresses at international conferences (Static Analysis Symposium 2012, Asian Symposium on Programming Languages and Systems 2008, Formal Methods for Industrial Critical Systems 2009).