ESBMC-Arduino: Closing the Deployment Gap for Formal Verification2 months agohttps://arxiv.org/abs/2607.08550本文介绍了ESBMC-Arduino，以弥合运行在微控制器（如Arduino）上的开源硬件PLC形式化验证中的部署差距。文章强调，缺乏硬件输入模型的朴素宽度感知验证会导致误报，如在123个真实程序中出现了44%的误报率。提出了一种基于硬件精准的验证方法，该方法利用声明式HAL描述符和健全的降低策略，以目标宽度解释算术运算，并将输入约束在硬件可实现范围内。该方法以ArduinoTool形式实现，在保持鲁棒性证明的同时消除了所有误报，并能通过可实现的反例检测罕见的宽度相关缺陷。