FMitF: Formal Verification & Implementation Stack for PLCs

Project Overview

This project advances a full formal-methods workflow from high-level differential dynamic logic models to executable PLC controller logic, with explicit links that preserve safety guarantees across design and runtime.

The public materials center on modular verification, monitor synthesis, and translation methods that connect model-level proofs with implementation artifacts used in realistic ICS settings.

The work builds on and extends prior HyPLC efforts, and informs follow-on work such as HyTwin for digital-twin-based security interventions.

Key Capabilities

• Bidirectional translation between verified hybrid-program models and PLC control-logic structure
• Runtime monitor synthesis that checks model-to-runtime compliance
• Modular verification workflows for scalable ICS controller development
• Reproducible experiment and evaluation artifacts rooted in water-treatment-style ICS case studies

Example Use Cases

• Design-time verification of PLC control logic against hybrid-system safety requirements
• Runtime validation of assumptions to detect deviations that invalidate offline proofs
• Evaluation of resilient control behavior under representative cyber-physical perturbations

Project Figures

Selected Publications

• HyPLC: Hybrid programmable logic controller program translation for verification

  Luis Garcia, Stefan Mitsch, Andr{\'e} Platzer · Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems (2019)

  ICCPS 2019 Best Paper Award Honorable Mention

• 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)

Research Themes