Reactive/interactive systems such as web applications and servers, real-time video streaming software, and Internet of Things (IoT) platforms are deeply embedded into all aspects of the modern world. Many program analysis techniques and tools have been created to analyze important temporal properties of these systems that span both safety (nothing bad will happen) and liveness (something good eventually happens). Unfortunately, modern static analyses are still limited in handling 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 they sometimes yield incorrect results.
This project is novel because of its theoretical and practical integration of static and dynamic approaches to analyze, localize, and repair temporal aspects of reactive/interactive systems.
The project's impacts are the development of new theories and algorithms, which will give rise to advanced methods for ensuring the safety/liveness of today's reactive/interactive software.
Nguyen will use the results of this research to develop new courses, senior design projects, and an interactive Jupyter book in programming languages and software engineering.
Nguyen will receive $400,000 total funding from NSF for this project. Funding began in December 2021 and will end in late September 2024.
###
About George Mason University
George Mason University is Virginia's largest public research university. Located near Washington, D.C., Mason enrolls 38,000 students from 130 countries and all 50 states. Mason has grown rapidly over the last half-century and is recognized for its innovation and entrepreneurship, remarkable diversity and commitment to accessibility. Learn more at http://www.gmu.edu .