Peter O'Hearn's research portrait

 

O'Hearn's current work is the areas of understanding concurrent programs and cybersecurity, doing proof work to make the attack surface smaller.

"I work on hard things that I don't understand and then figure out things I never knew I was going to figure out," says Peter O'Hearn. The math ends up teaching me those things, usually."

O'Hearn is Royal Academy of Engineering/Microsoft Research Professor and Head of Programming Principles, Logic and Verification Research Group at the UCL's Computer Science Department.

He may sound more like an artist than a theoretical computer scientist, but O'Hearn's seminal work in separation logic, which along with work done by John Reynolds at Carnegie-Mellon, co-founded the field, came about in just that way. His best-effort description of the thought process is that the math told him things he didn't know he was looking for.

O'Hearn's particular research focus, program verification, is an old topic for theorists. Yet his goal is practical: "We want to make breakthroughs such that they can be put in tools that everyday programmers can use," he says.

In fact, the point of separation logic is to prove the absence of bugs in a piece of software. It involves analysing what's going on in memory, something most people thought was impossibly complicated when he began work in this field. The reason: as computers use pointers to connect one area of memory to another, the resulting interconnections become as complicated as a tangle of spaghetti.

"Everybody thought that memory was so entangled that you couldn’t pull it apart," O'Hearn says. "I used to have people laugh at me when I said I was going to do this in a way that scales, and then they would show me some complicated structure and say, you're never going to do it. The key thing was not pulling all the strands of spaghetti apart, but cutting them in two."

If it sounds like that technique would break the memory, that's the hard part: "It doesn't, because we cut the links but don't follow them off the end. So we don't fall off into the ocean" – that is, wind up in a core dump. "We just did some mathematics and made sure to cut it into little chunks that don't cause us to fall into the ocean."

When he first came up with separation logic – around 2000, while he was a professor at Queen Mary – O'Hearn was working in one of the most theoretical of computer science subjects, programming language semantics.

"I was thinking hard about the mathematical structures of programs, and then I don't know how, but I discovered that certain mathematical properties were true, which implied that tools could exist that we didn't know about. The mathematics told me answers that I wasn't searching for."

At the time, he was trying to understand the structure of low-level systems programs, whose structures are not formalised.

"My hypothesis is that humans have designed for example operating systems with an intuitive beautiful structure," he says. "It's partly because the scale of what they're doing is so huge. If it were really a mess they wouldn't be able to do it. The human mind couldn't  comprehend that size of things without there being an elegant structure. And if we can discover that structure we will have a leg up on constructing more secure systems."

O'Hearn's current work is in two areas. First is understanding concurrent programs, essential as improvements in computing power rely more on multiple processors than increasing clock speed.

"These are the hardest programs for humans to understand," he says.

The second area is cybersecurity, doing proof work to make the attack surface smaller.

Research highlights

O'Hearn's most significant papers are two that set out separation logic. The first is BI as an Assertion Language for Mutable Data Structures (PDF), written with Samin Ishtiaq and published in the proceedings of the Symposium on Principles of Programming Languages (POPL) 2001. O'Hearn describes this paper as the second step in a series of three that progressively scaled up and completed the ideas behind separation logic. This paper won the 2011 Most Influential POPL Paper award

The second is Local Reasoning about Programs that Alter Data Structures (PDF), presented at the 2001 Annual Conference of the European Association for Computer Science Logic (CSL).

"Local Reasoning showed how to pull memory apart, and how the logic or reasoning – the proofs – can concentrate on little bits of memory at a time," he says. "We showed how to stitch together many little proofs to make a big proof. BI was really a conceptual breakthrough; Local Reasoning finished it off and made it perfect."

A third key paper is O'Hearn's 2011 paper, written with Cristiano Calcagno, 2012 Needham Prize winner Dino Distefano, and Hongseok Yang, Compositional Shape Analysis by means of Bi-Abduction (PDF), published in the Journal of the Association for Computing Machinery. This paper automates the theoretical ideas developed in the earlier two using the scientific method developed by philosopher Charles Peirce, who divided reasoning into three types: deduction, induction, and abduction.

"What the paper does is cycle through these three concepts in order to discover   properties of computer programs," O'Hearn says. "It looks at code like a scientist would look at the natural world and makes hypotheses. It automates the scientific method."

The effects of O'Hearn's work can be clearly seen in a few numbers. In 1999, the tools for proving that memory won't be corrupted were limited to about ten lines of code. By 2008, their tools could verify 10,000 lines of code – enough for the device drivers that account for most Windows crashes. Another breakthrough between 2007 and 2012 made it possible to verify partial properties of 10 million lines, approximately the amount of code in a smartphone. 

This page was last modified on 20 Dec 2012.

Dr Peter O'Hearn

 

Office:

66GS.G2D

Tel:

+44 020 7679 5777

Fax:

+44 020 3108 5040

Email:

P.OHearn (at) cs.ucl.ac.uk

Website