Digital Twins & Formal Verification
Formal and hybrid systems verification; fidelity-aware digital twins; verification-driven testbed design.
Funded Projects
SPHERE CPS Enclave: Reconfigurable Testbed for CPS
SPHERE CPS Enclave is a reconfigurable, remotely accessible industrial-control experimentation environment for repeatable and shareable cybersecurity studies spanning PLC logic, SCADA/HMI interaction, process telemetry, and configurable network behavior.
FMitF: Formal Verification & Implementation Stack for PLCs
FMitF develops a provably correct stack that links formal hybrid-system models to PLC implementations, combining verified runtime monitoring with bidirectional model-code translation for industrial control systems.
Featured Publications
SPHERE CPS Enclave: A Reconfigurable Testbed for Industrial Control System Security Experimentation
Luis Garcia, Jelena Mirkovic, David Balenson, et al.
Proceedings of the ACM/IEEE 16th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2025) • 2025
HyTwin: Hybrid Program Semantics for Digital Twin-Based Security Interventions in Industrial Control Systems
Jainta Paul, Stefan Mitsch, Luis Garcia
NASA Formal Methods Symposium • 2025
Collaborative Research: FMitF: Track I: A Formal Verification and Implementation Stack for Programmable Logic Controllers
Luis A Garcia
NSF Award Number 2425711. Directorate for Computer and Information Science and Engineering • 2023
$\{$PAtt$\}$: Physics-based Attestation of Control Systems
Hamid Reza Ghaeini, Matthew Chan, Raad Bahmani, et al.
22nd International Symposium on Research in Attacks, Intrusions and Defenses (RAID 2019) • 2019
Related Publications
PhysioGAN: Training High Fidelity Generative Model for Physiological Sensor Readings
arXiv preprint arXiv:2204.13597 • 2022
Collaborative Research: FMitF: Track I: A Formal Verification and Implementation Stack for Programmable Logic Controllers
NSF Award Number 2220312. Directorate for Computer and Information Science and Engineering • 2022
A Hybrid Neuro-Symbolic Approach for Complex EventProcessing
arXiv e-prints • 2020
A Hybrid Neuro-Symbolic Approach for Complex EventProcessing
arXiv preprint arXiv:2009.03420 • 2020
HyPLC: Hybrid programmable logic controller program translation for verification
Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems • 2019
A hybrid neural-symbolic approach to uncertainty-aware complex event detection
Workshop on Distributed Analytics InfraStructure and Algorithms for Multi-Organization Federations 2019 • 2019