Resources
Software & Benchmarks
SENTINEL
Framework for multi-level formal safety evaluation of foundation model-driven embodied agents, grounding natural-language safety requirements in temporal logic and evaluating safety at semantic, plan, and trajectory levels; focusing more on LLM/VLM-driven planning and reasoning.
ManiGuard
Framework for specification-grounded safety evaluation and improvement of foundation model-driven embodied agents, including a safety-centric benchmark ManiGuard-Bench and a safety-annotated trajectory-generation pipeline for model fine-tuning; similar methodology as SENTINEL but focusing more on VLA-driven, contact-rich robotic manipulation.
POLAR / POLAR-Express
Polynomial arithmetic framework for formal reachability analysis and safety verification of neural-network controlled systems.
SAW
Safety analysis tool for verifying nonlinear weakly-hard systems that may occasionally miss deadlines in a bounded manner.
Talks
Know the Unknowns: Design Automation for Learning-Enabled Cyber-Physical Systems
Other Resources
- IEEE Council on Electronic Design Automation (CEDA) — Qi Zhu serves as VP of Publicity
- National Academies Standing Committee on Personal Protective Equipment for Workplace Safety and Health — Qi Zhu serves as a committee member