FORTRESS: Formal Techniques for Resilient and Secure Systems
We study formal methods for correctness and security of computer systems, with a focus on cyber physical systems. We develop reasoning techniques and enforcement mechanisms that support secure and dependable systems.
About
FORTRESS is a research group at UNC Charlotte working on formal foundations and tools for secure and reliable systems. Our work emphasizes mathematical proofs and verification techniques to show that no attack strategy can cause a system to misbehave.
Principal Investigator: Jian Xiang, Assistant Professor, Software and Information Systems, College of Computing and Informatics.
Contact
Research themes
- Formal methods for security and resilience in cyber physical systems
- Quantitative robustness analysis under sensor and timed attacks
- Relational reasoning in dynamic logics
- Information flow analysis and language based security
- Runtime enforcement mechanisms grounded in formal guarantees
Selected recent publications
-
Formal Robustness for Cyber Physical Systems under Timed Attacks
IEEE CSF, 2025 -
Extending Dynamic Logics with First Class Relational Reasoning
NASA Formal Methods Symposium, 2025 -
Measuring Robustness in Cyber Physical Systems under Sensor Attacks
Nonlinear Analysis: Hybrid Systems, 2025
For a full list, see here.
People
- Jian Xiang (PI)
- Tahmid Chowdhury (PhD)
- Utkarsh Parashar (master)
- Sai Phanindra Kothuri (master)
- Ramnarayanan Sankar (Alumni)
Join the lab
We welcome self motivated PhD students and undergraduates interested in building secure and pragmatic systems using formal methods.
- If you are at UNC Charlotte, email or stop by to chat
- If you are not yet admitted, apply through the usual channels and then reach out
- When emailing, please include your interests and why they align with our work
More details: Information for prospective students
News
- We will hold group seminar at Woodward 309 most Fridays between 12-1pm. See this calendar for the schedule. Feel free to drop by.