Eric Koskinen Receives $593K NSF Grant to Develop Scenario-Based Formal Proofs for Concurrent Software
The computer science professor will develop rigorous reasoning tools to help programmers demonstrate the accuracy of their work
Eric Koskinen — associate professor and Charles Berendsen junior professor in the Department of Computer Science — recently received a $593,022 National Science Foundation (NSF) grant to develop formal, yet user-friendly, proofs for verifying the accuracy of concurrent software in his project formally titled “CISE-ANR: SHF: Small: Scenario-based Formal Proofs for Concurrent Software.” The grant is in collaboration with Professor Constantin Enea at École Polytechnique and jointly supported by the French Agence Nationale de la Recherche.
Modern software takes advantage of computers with multiple processors by using concurrent programming, in which more than one process is executed at the same time.
Researchers have developed mathematical reasoning techniques to prove that their concurrent programming is correct, but these techniques require complex mathematical manipulations and rules that are often difficult to understand. In contrast, algorithm designers in the distributed computing community (in which multiple computers work together to complete a task) argue for the accuracy of their work in an easier-to-understand manner by describing a few key example scenarios of how different simultaneous tasks occur correctly.
These arguments describe certain critical scenarios that are approachable to programmers who can use them to understand the correctness of their code. Unfortunately, these scenario-based correctness arguments lack rigor and, thus far, cannot be expressed as formal mathematical proofs.
Koskinen’s project will bridge this gap by developing a formal yet approachable method for proving concurrent programming using scenario-based reasoning. This method will allow everyday programmers without a background in formal methods to verify their concurrent software’s correctness. His project will develop theories, algorithms and tools that demonstrate that it is possible to formalize, and even automate, rigorous scenario-based proofs for concurrent software.
“I am excited about this project because it will lead to real tools that could be used by everyday programmers to improve their implementations of critical software. Consequently, concurrent software will more safely exploit multicore architectures. We aim for full automation, along with explainable results,” said Koskinen.
He continued, “The tools resulting from this research will directly consume source code and, through a combination of new algorithms and reasoning techniques, discover representative scenarios automatically. This already may provide a proof, but the programmer may now wish to ask questions about specific executions, and an interactive mode of our tool will consume such queries and generate explanations as to how a specific execution corresponds to a scenario.”
Koskinen will apply his techniques to important real-world systems such as web and database servers and applications. These systems are omnipresent: for example, we interact with web and database servers daily. Indeed, much of humanity’s well-being critically depends on these servers operating correctly.
Travel scholarships for students from historically underrepresented groups
In addition to the concurrent software grant, Koskinen has received a $52,000 NSF award for his project “Collaborative Research: Verification Mentoring Workshop at Computer Aided Verification,” with Purdue University as prime.
This project offers travel grants for students to attend the Verification Mentoring Workshop (VMW) and the International Conference on Computer Aided Verification (CAV) last year in Paris and this year in Montreal. CAV is one of the premier conferences in computer science, dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. The purpose of VMW is to provide mentoring and career advice to early-stage graduate students, to attract them to pursue research careers in the area of computer-aided verification. Preference will be given to women and students belonging to underrepresented groups.