ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs
Summary
The paper ESBMC-Arduino addresses the deployment gap for formal verification of IEC 61131-3 on low-cost MCUs (Arduino/OpenPLC-based) by introducing hardware-faithful verification. It presents a HAL-based approach to constrain inputs to hardware-realizable ranges and demonstrates that this reduces false alarms, improving robustness proofs across a corpus of programs.