Computer Science Professor Eric Koskinen and Research Scientist Ton-Chanh Le Receive $399,995 National Science Foundation Grant for Dynamic Temporal Analysis
The collaboration with Yale University and George Mason University aims to advance methods for ensuring the safety of modern software
Assistant Professor Eric Koskinen and Research Scientist Ton-Chanh Le, both from the Department of Computer Science, recently received a grant of $399,995 from the National Science Foundation (NSF) for their project “Collaborative Research: SHF: Medium: Ensuring Safety and Liveness of Modern Systems through Dynamic Temporal Analysis.” This is part of a joint research undertaking in collaboration with Yale University and University of Nebraska-Lincoln.
Reactive and interactive systems like web applications and servers, real-time video streaming software, and IoT platforms are deeply embedded into all aspects of our modern world, however, modern static analyses are still limited in their ability to handle complex program semantics that often appear in many real-world applications. They support only simple properties, produce false positives, or do not scale to large programs.
Recent dynamic or "data-driven" approaches address several shortcomings of static analyses to analyze more complex program properties more efficiently, yet sometimes yield incorrect results.
Koskinen and Le’s project aims to develop new theories and algorithms around practical integration of static and dynamic approaches to analyze, localize, and repair temporal aspects of reactive/interactive systems. The success of such a project could lead to advanced methods for ensuring the safety/liveness of today's reactive/interactive software.
“The project's use of dynamic analysis enables inference of expressive properties of these programs, while the use of static verification allows for validation of those inferred properties,” explained Koskinen. “Furthermore, static verification and dynamic learning mutually inform and bolster the power of each other, allowing for safety/liveness analyses, and even to localize faults and synthesize repairs for temporal defects.”
Koskinen says the methods being developed are embodied in a growing collection of automated tools to soon be released publicly.
“The integration and interaction between dynamic learning and static verification can give rise to new methods, algorithms, and tools that can be applied to a wider range of programs and make temporal reasoning more scalable to real-world applications and accessible to software developers without knowledge in program analysis,” Le added.
This project is a collaboration with Yale and George Mason University.
Learn more about computer science at Stevens: