Researcher Joins ITTC Effort to Build More Reliable Software
By Michelle Ward
Neil Sculthorpe began a two-year post-doctoral research position with ITTC's Functional Programming Group this spring. He joined the Haskell Equational Reasoning Model-to-Implementation Tunnel (HERMIT) project. ITTC investigator Andy Gill's group is working to dramatically reduce all-too-common bugs and glitches that occur in current software. Finding ways to reduce errors could potentially save billions of dollars annually.
"Neil is a welcome addition to our team. He brings a depth of theoretical understanding of the fundamental ideals behind the construction of high-assurance software. The HERMIT project will build on his previous work and allows us to use the combination of software engineering and mathematics to make the evaluation of software more manageable," said Dr. Gill, who received a $500,000 NSF grant this fall for HERMIT. "When you are building large systems with millions of lines of code, finding errors can be very difficult. Unreliable software then hurts companies' reputations and costs them customers."
HERMIT mathematically, or formally, analyzes each step of development, providing rigorous connections between system requirements and the programming details of real applications. While system requirements and programs are typically written in two different computer languages and often evaluated in a third, HERMIT provides a common foundation that generates evidence that the description and action match. These continuous checks and balances make it much harder for errors to be introduced.
Dr. Sculthorpe, who received his Ph.D. in Computer Science this past summer from the University of Nottingham, will focus on worker/wrapper transformation. This is a verification technique for connecting specifications to efficient implementation. He says a major goal of the project is to make applying transformations as painless as possible, allowing the HERMIT tool to be used by non-expert users.
For more information, contact ITTC.