ESBMC-Arduino: Closing the Deployment Gap for Formal Verification

I developed ESBMC-Arduino to bridge the gap between abstract safety proofs and real-world hardware constraints on devices like Arduino and OpenPLC. Existing verifiers often generate false alarms by ignoring physical sensor limits and finite arithmetic. My new approach uses a hardware-faithful model to eliminate these errors while detecting genuine overflow defects that could silently suppress critical safety actions in industrial control systems.

"An unbounded input model fabricates alarms that no environment can trigger."