From Computer Science magazine, fall 2014

Peter O’Hearn (BSc’85) lives in London, England, and has landed a job at Facebook building and deploying static analysis tools – notably using Infer, a static analyzer acquired when Facebook took over O’Hearn’s startup.

Last February the social media site celebrated its tenth anniversary, and today, Facebook has over 1.32 billion monthly active users, and over 7,185 employees worldwide.

Dalhousie University Computer Science alumnus Peter O’Hearn is among the billions of users who have a Facebook profile page. He, like many others, regularly posts updates to his page. For example, according to Facebook, O’Hearn caught a number of squid in St. Margaret’s Bay, N.S. this past summer.

The Halifax native is well versed in Facebook. But his social media expertise spans beyond the occasional status update.

Also noted on his profile page is his place of employment: Facebook.

Based in the company’s London, England office, O’Hearn was hired to work for the popular social media site following the acquisition of his startup company, Monoidics, in 2013 by Facebook. Monoidics was created in 2009 by O’Hearn and two colleagues, Cristiano Calcagno and Dino Distefano. Their company marketed Infer, the separation logic-based static analysis tool.

Separation logic is a theory that facilitates scalable reasoning about programs, particularly concerning the way they access and mutate memory and other dynamic resources.

Separation logic was developed jointly by O’Hearn and the late Prof John Reynolds from Carnegie Mellon University.

O’Hearn says the creation remains his greatest achievement.

“With separation logic a range of programs that previously only had messy, complicated specifications and proofs became easy to deal with. This opened up new possibilities both in theoretical and practical work,” says O’Hearn.

“In addition to its significance, the work on separation logic was (to my mind) pretty. It is a compact theory based on a few primitives,that nonetheless provides the power to go much further on difficult problems than previous more-complicated approaches.”

Today O’Hearn works with a team at Facebook building and deploying static analysis tools. These are software tools that crawl over code searching for bugs and attempting to prove properties of the code. The team uses separation logic in their work, particularly with the Infer static analyzer.

For O’Hearn, landing a job at Facebook has been the icing on the cake. He remembers his first visit to the company’s main headquarters in Hacker Way, California.

“When I first arrived it was a jawdropping experience,” he recalls. “There were restaurants, cafes, people driving around on bicycles and skateboards, there was graffiti and other art on the walls of the offices, there was funky music playing before seminars and in lunch areas. I thought it felt like Disneyland. Only later did I find out that Facebook actually hired Disney consultants to help give it its amazing look and feel.”

He says most importantly, he was inspired by the people he met: hundreds of employees working enthusiastically to make an impact on the company.

“It was amazing,” he says. “It’s an extremely positive atmosphere and there are a lot of intelligent people to engage with and challenging problems (to solve).”

The work ethic within the company is one O’Hearn has always instilled within himself. He says he likes a challenge and sets his standards very high.

“We purposely choose difficult goals so it’s hard to achieve them,” he says. “We challenge ourselves. It feels great when you actually achieve those goals.”

He says working at Facebook has taken him one step closer to achieving his next goal.

“A career goal of mine has been for program verification, based on logics of programs, to have broad realworld impact,” he says. “It should help programmers write more reliable code and therefore impact the people that use this code. Over a billion people use Facebook, and there is a great programming culture here, making this an ideal situation for me.”