NSF grant supports indexing programming project at Appalachian

Posted Feb. 16, 2018 at 4:55 p.m.

BOONE, N.C. — Dr. Patricia Johann, professor in Appalachian State University’s Department of Computer Science, was awarded $463,504 in funding from the National Science Foundation (NSF) for her project exploring new foundations in indexed programming that will help ensure secure and reliable software systems.

Johann said testing of programs has dominated the last 50 years of software development, but the next 50 years will see an increased demand for provably correct software.

“This is partly because modern applications are increasingly safety critical, partly because testing is, by its very nature, only a partial correctness guarantee and partly because programming language technology has now advanced to the stage where it is feasible to formally verify critical programs,” she said.

“Language-based verification uses a language’s type system to guarantee program correctness so that type checking a program becomes tantamount to verifying its correctness. Thus, the more program properties a type system can express, the more the compiler can automatically verify.”

According to Johann, indexed programming is a key technique for using a language’s type system to express more and more sophisticated properties of programs.

“Indexed programming uses the extra information present in type indices to help close the so-called semantic gap between what programmers know about their programs and what type systems can express about them,” she said.

In her commentary on the project, Johann writes, “The intellectual merits of this project lie in providing a principled methodology for transferring knowledge about effective programming and proving between languages supporting type indexing of types and those supporting term indexing of types, developing a semantic framework that enhances researchers’ and practitioners’ understanding of the nature of indexed types in general, and opening the way for new forms of indexing that can enforce even greater correctness guarantees.”

She said the broader impact of this project is to use indexed types to develop better and more widely applicable formal program verification methods, and, thereby, to help ensure that even large and sophisticated software systems are safe and reliable.

“Because it will lead to provably correct and secure software, this project has the potential to impact any application area, and thus any sector of the economy, for which such software is paramount,” said Johann.

About the Department of Computer Science

Appalachian’s Department of Computer Science provides a rigorous, high-quality education that prepares students for the computing industry or graduate education. It offers a Bachelor of Science degree in computer science, which is accredited by the Computing Accreditation Commission of ABET, and a Master of Science degree in computer science. Learn more at https://compsci.appstate.edu.

About Appalachian State University

As the premier public undergraduate institution in the state of North Carolina, Appalachian State University prepares students to lead purposeful lives as global citizens who understand and engage their responsibilities in creating a sustainable future for all. The Appalachian Experience promotes a spirit of inclusion that brings people together in inspiring ways to acquire and create knowledge, to grow holistically, to act with passion and determination, and to embrace diversity and difference. Located in the Blue Ridge Mountains, Appalachian is one of 17 campuses in the University of North Carolina System. Appalachian enrolls more than 20,000 students, has a low student-to-faculty ratio and offers more than 150 undergraduate and graduate majors.