ESBMC-Arduino Brings Formal Verification to Embedded Developers

ESBMC-Arduino is a new tool that extends the ESBMC model checker to verify Arduino programs for bugs like buffer overflows and division by zero. It aims to close the gap between formal verification research and practical embedded development. The tool is open-source and targets the widely-used Arduino platform.