Towards Integrity and Reliability in Embedded Systems: The Synergy of ESBMC and Arduino Integration

Rafael G. Silvestrim, Felipe V. Trigo, Williame Rocha, Michael R. S. Vieira, Jogno V. Junior, Otoniel da C. Mendes, Rafael Menezes, Lucas Cordeiro

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Downloads (Pure)


We’ve developed and evaluated a new method called ESBMC-Arduino that combines the ESBMC model checker with the Arduino hardware platform. This verification method helps ensure the safety and safety of Arduino C code by finding and, to some extend, preventing errors, thus making the entire system code more reliable. This collaboration is particularly useful for critical embedded systems, improving safety analysis, and promoting contract-driven development practices. We also advocate that our proposed method is valuable for teaching and advanced research in formal verification and embedded systems safety. Our experimental results show that using ESBMC for formal verification of Arduino code leads to better error detection, more accurate code, and increased reliability. This demonstrates that ESBMC-Arduino effectively identifies software vulnerabilities (e.g., memory management and overflow prevention) and enhances the safety of embedded systems. Index Terms—ESBMC, Arduino, Embedded Systems, Formal Verification, and Software safety.
Original languageEnglish
Title of host publicationXIII Brazilian Symposium on Computing Systems Engineering
Publication statusE-pub ahead of print - 24 Nov 2023


Dive into the research topics of 'Towards Integrity and Reliability in Embedded Systems: The Synergy of ESBMC and Arduino Integration'. Together they form a unique fingerprint.

Cite this