Stephen F. Siegel, assistant professor in the Department of Computer and Information Sciences at the University of Delaware, has been named a winner of the prestigious National Science Foundation Faculty Early Career Development Award for his research to ensure the accuracy of scientific software.
Siegel said he was pleased to receive the award, which includes a $412,000 grant, noting, “It’s very encouraging because the judges are the leading experts in the field and this says they think this work is important.”
Scientific practice has been radically transformed by computation, said Siegel, who directs UD’s Verified Software Laboratory, and many observers now place computational simulation on an equal footing with the two traditional approaches to scientific discovery — experimentation and theory.
But while there are long established and rigorous criteria for validating experiments and mathematical reasoning, he said, the same is not true for simulation. Published reports of simulation-based research typically say little or nothing about the software, its qualities, or what was done to ascertain its correctness. The software is rarely examined by reviewers or other researchers, and in some cases is not even made available to them.
This situation is particularly troublesome in light of the substantial evidence that scientific software is, in general, as unreliable as any other type of software.
“Computers are being used in every area of science and engineering now,” Siegel said. “Climate modeling, weather prediction, drug discovery, the engineering of cars, airplanes, buildings — these are just a few examples, and obviously these applications are of immense importance to society.”
The expanded use of computers “has made possible incredible advances,” he said, “but it also comes with risks. We know that most software is very ‘buggy,’ and the software written and used by scientists is no different in that regard. Defective software can lead to inaccurate results, invalid conclusions, and in the worst case, loss of life.”
Work in the field has been sparse. “There has been a lot of work in reliability of other kinds of software, but not too much for scientific software,” Siegel said. “It turns out to be extremely difficult to verify scientific programs for several reasons. First, the numerical algorithms they use are extremely complex as they are often written for parallel computers, perhaps with thousands of processors. The programs are difficult to test because you usually don’t know what the correct answer is supposed to be, so you don’t have a way to tell if the result of a test execution is right.
“Also, there has been an unfortunate cultural divide between the scientific and computer science communities. Most scientists haven’t studied much computer science and are skeptical the field has anything to offer them, and most computer scientists know little about the application sciences and the techniques they use, and so have a hard time designing techniques that are effective for scientific software. Fortunately, there are some signs that this gulf is narrowing.”
Siegel’s research focuses on developing a set of integrated techniques for the specification and verification of scientific software. Drawing on ideas from model checking, symbolic execution, and other formal methods, these will include:
- New techniques to efficiently check for the presence of deadlocks, race conditions, improper use of parallel programming libraries, and other generic defects in scientific programs;
- Techniques to specify and verify the order of accuracy of numerical programs, such as those used to solve systems of differential equations; and
- New techniques to verify the functional equivalence of two scientific programs, including programs with unbounded loops, and programs with (shared-variable and/or message-passing) parallelism.
These techniques will be realized in a new tool suite, the Toolkit for Accurate Scientific Software (TASS), which will be made publicly available under an open source license.
The part of TASS dealing with order of accuracy involves another member of the UD faculty, Louis Rossi, associate professor in the Department of Mathematical Sciences, who has expertise in applications. “Lou has a deep understanding of the techniques that go into solving differential equations and the kinds of properties the developers want to verify,” Siegel said. “We computer scientists in the Verified Software Lab then devise techniques for automatically verifying those properties.”
Siegel said it is his hope that the research “will give computational scientists a tool to check that their programs are correct, or find and report bugs if a program is incorrect. I hope such tools will become a routine part of development of scientific software. Ultimately this will give all of us much greater confidence in the results produced by computer simulations and save a lot of time and effort debugging those programs.”
Siegel said he decided to make TASS available through open source because “the free exchange of ideas is of the utmost importance in academic inquiry. If I make claims that TASS can do such-and-such, anyone should be able to download TASS and check for themselves if what I claim is true. If they want to use TASS or extend it in some way they should be able to do so without any obstacles.”
Siegel joined the UD faculty in 2006 after serving as a visiting assistant professor at both Northwestern University and the University of Massachusetts Amherst, where he also was a senior software engineer and senior research scientist.
He received a bachelor’s degree and doctorate in mathematics from the University of Chicago and a master’s degree in mathematics from Oxford University.
A mathematician by training, he became interested in software engineering at the University of Massachusetts in the late 1990s and took a job as a software engineer and then research scientist in the Laboratory for Advanced Software Engineering Research (LASER). Software verification is one of the research areas in which LASER specializes.
“Mathematicians have a very high standard for truth and correctness — everything must be proved — so it was a natural transition to carry that attitude over to the development of software,” he said.
Siegel directs the Verified Software Laboratory, a software engineering research laboratory in the Department of Computer and Information Sciences housed in Ewing Hall. He said the lab is “exploring ways to make extremely reliable software, especially for computational science. We also produce and release software packages ourselves, for example the MADRE library, which is used for data redistribution in massively parallel computers.”
Siegel is the second person in the department to receive an NSF Career Award this year, joining John Cavazos.
Article by Neil Thomas
Photos by Ambre Alexander