He worked with the Formal Methods Research Program within the Safety Critical Avionics Division at NASA Langley Research Center from May to August.
Siratt was able to secure an internship with the space agency thanks to help from his professors. Dr. Lakeshia Jones, assistant professor in the Department of Mathematics and Statistics, supervised Siratt’s independent studies and encouraged him to develop research topics and search for specialized internship opportunities.
“Dr. Jones encouraged me to think about research topics, and I did a practice research statement,” he said. “The topic I got interested in seemed to have obvious applications for aerospace. The Arkansas Space Grant Consortium said that NASA has internships, so I reached out to them and had a conference call to some researchers at NASA Langley Research Center. They invited me to apply, and the next thing I knew they were asking what kind of computer I wanted when I got there.”
In addition to the help Jones provided, Dr. Steven Minsker, professor of computer science, helped Siratt prepare for the internship by supervising an independent study.
“Without Dr. Jones and Dr. Minsker, I would not have had the background to make the progress I made while at Langley,” he said. “My NASA mentors were very impressed with my skills and knowledge, and none of that would have been possible without the willingness of these faculty members to supervise relevant independent study.”
His internship was supported through a Workforce Development grant from the Arkansas Space Grant Consortium. He worked with Dr. Anthony Narkawicz, Ricky Butler, and Dr. Cesar Munoz from NASA.
At the research center, Siratt was assigned a three-month project that he wrapped up in five weeks. Siratt studies automated theorem proving, a subfield of artificial intelligence and mathematical logic that deals with proving mathematical theorems with computer programs.
Siratt and his mentors redesigned and improved a library of trigonometry proofs used to prove mathematical concepts the Formal Methods team is using to verify algorithms for air traffic control systems. This work was performed in the prototype verification system (PVS) theorem prover, a system which allows users to rigorously prove mathematical statements.
“Let’s say we are having a debate with a very meticulous person who wants you to justify everything,” Siratt said. “That is what it’s like to justify everything to a computer. We program a drone or autopilot system or air traffic control system, and the computer wants you to prove your mathematical concepts. We use trigonometry a lot. We don’t want to have to re-prove trigonometry to the computer every time, so we have a trigonometry library where the proofs are contained.”
Siratt and his mentors generated more than 100 trigonometry proofs during his internship.
“The computer is going to hammer and hammer you on the details of the computer programming until it is convinced it is right,” he said. “You can look at my work for the summer as finding ways to argue the truth of the facts of trigonometry in as simple a way as possible.”
With the additional time, Siratt was able to work with other research projects and explore his own research topics with the other scientists.
“I really enjoyed the internship,” he said. “It was a great atmosphere with great people to work with. People are coming in and out and discussing ideas. The people enjoy what they do and are self motivated.”
Siratt is planning to apply for another internship at NASA Langley Research Center for summer 2018.
In the upper right photo, John Siratt (right) and his wife, Chassidy (left), attend the 2016 Fribourgh Award Reception at Pleasant Valley Country Club. Photo by Lonnie Timmons III/UA Little Rock Communications.