Scaling Trustworthy Formal Verification in NextG and Beyond
As 5G and NextG systems grow in complexity, ensuring security and correctness requires verification approaches that are both scalable and trustworthy. This talk highlights recent progress from the MACC Lab at Stevens Institute of Technology, developed with DARPA, including our new system Auto-modeling of Formal Verification with Real-world Prompting (AVRE). AVRE leverages large language models (LLMs) to transform protocol descriptions into dependency graphs and formal models, using cross- and self-attention with transformer-based reasoning to resolve ambiguities, capture design intent, and establish quantifiable dependencies. Integrated with our HyFuzz hybrid fuzzing platform, AVRE closes the loop between formal modeling and experimental validation. Together, these advances demonstrate a robust, AI-assisted pipeline for formal verification and vulnerability detection in cyber-physical and wireless systems, paving the way for practical assurance frameworks in contested and mission-critical environments.
Date and Time
Location
Hosts
Registration
-
Add Event to Calendar
- Contact Event Hosts
-
Hong Zhao (zhao@fdu.edu), Alfredo Tan (tan@fdu.edu)
- Co-sponsored by Fairleigh Dickinson University
Speakers
Ying Wang of Stevens Institute of Technology
Title: Scaling Trustworthy Formal Verification in NextG and Beyond
As 5G and NextG systems grow in complexity, ensuring security and correctness requires verification approaches that are both scalable and trustworthy. This talk highlights recent progress from the MACC Lab at Stevens Institute of Technology, developed with DARPA, including our new system Auto-modeling of Formal Verification with Real-world Prompting (AVRE). AVRE leverages large language models (LLMs) to transform protocol descriptions into dependency graphs and formal models, using cross- and self-attention with transformer-based reasoning to resolve ambiguities, capture design intent, and establish quantifiable dependencies. Integrated with our HyFuzz hybrid fuzzing platform, AVRE closes the loop between formal modeling and experimental validation. Together, these advances demonstrate a robust, AI-assisted pipeline for formal verification and vulnerability detection in cyber-physical and wireless systems, paving the way for practical assurance frameworks in contested and mission-critical environments.
Biography:
Dr. Ying Wang is an Associate Professor at Stevens Institute of Technology whose research centers on cyber-physical system (CPS) assurance in advanced wireless networks. She brings extensive experience across academia and industry, integrating expertise in wireless communications, formal verification, and quantum computing. Her work focuses on advancing scalable, secure, and resilient CPS systems, including NextG networks, through cross-layer design and rigorous assurance frameworks. She also explores how quantum computing can be incorporated into assurance pipelines and vulnerability detections. Committed to bridging theory and practice, Dr. Wang emphasizes technology transition to ensure that her research addresses real-world challenges in CPS security and resilience.
Email:
Address:United States
Agenda
Fairleigh Dickinson University
1000 River Road, Building: Muscarelle Center, Room Number: 105
Teaneck, New Jersey, United States 07666
For additional information about the venue and parking, please contact
Dr. Hong Zhao