David took three months out of his PhD to work at the NASA Ames Research Center located in California's Silicon Valley. The Ames Research Center has led NASA’s research in aeronautics development and exploration technology for the last 75 years.

About DavidDavid Butler

David is a third year PhD student at the Turing, affiliated with the University of Edinburgh. His main research interest lies in the formal verification of cryptography working with the proof assistant Isabelle. Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. David’s internship with NASA enriched his PhD studies as he was able to gain further experience using Isabelle in a different context to his research to date.

About the internship

David was working in the Ames Safety and Assurance Research Group within the Robust Software Engineering Group of NASA’s Intelligent Systems Division. Reflecting on his experience, he says:

“I was working on the safety cases of unmanned aircraft - a safety case is a rigorous and explicit justification for why a system meets specific safety properties - and in particular, I was working on the formalisation of the safety cases, meaning the goal was obtaining machine checked proof (using Isabelle) that the safety properties hold. In simple terms, my work involved using logical programs to analyse the safety of NASA’s unmanned aircraft.

“One such safety property is ensuring there are no mid-air collisions. Airspace is becoming increasingly congested, so the risk of collisions is growing and consequently measures need to be put into place to avoid such collisions. My work focussed on ensuring unmanned aircraft stayed safe by avoiding collisions with ‘intruder’ aircraft; these are not necessarily aircraft with malicious intent, but simply aircraft that may be flying in the region of the unmanned aircraft. I was working on verifying the correctness of the systems that ensure there is sufficient time to avoid a collision from when an intruder aircraft is detected.”

David talks about his area of research:

“I specialise in formally verifying proofs. A proof is a logical chain of reasoning, it is evidence establishing a fact. My goal is to obtain proofs checked by a proof assistant. This means a computer has verified the proof and not humans (humans make mistakes, computers generally only make mistakes when humans tell them to do the wrong thing!). We can then say we have a ‘machine-checked’ proof, which gives us a higher assurance of correctness.

The lead in the Assurance Research Group, Ewen Denney, added:

“David's work formalising some of the reasoning in our safety case was really useful, and helped us discover an aircraft encounter situation that we had not accounted for.”

Enriching my PhD

“At NASA I was able to gain experience working in an applied research group, whereas until that point I’d worked solely in academia. One of the main differences between the two environments is that outside pure academia, the desire for a solution is greater than the need for something to be perfect. In academia, one is often striving for the perfect way to do something. This is not always the case elsewhere, where a working solution is more important. Proofs do not have to be perfect or elegant – they have to work, but an elegant solution is of course much nicer!

"Working in a related – though different - area has provided food for thought for life after my PhD. I’ve gained valuable insight in terms of carving a career in my area of work and it was exciting to be able to use the skills I have within an applied setting. The internship also created opportunities for international collaborations through which to undertake further work in this area.”

“I found that taking some time out from my PhD enhanced my PhD research too, as it provided an opportunity to step back and review my work and relieved some of the pressure of continually contributing to it. I now have a new energy and enthusiasm back at the Turing and have returned with fresh ideas for my PhD research.”

“The experience of living and working abroad was another highlight and something I had not done before – I would recommend it to anyone. In short, my internship with NASA has been hugely beneficial in many ways and I would certainly urge any of my peers at the Turing to enrich their PhD on a similar placement.”