Embedded Systems Summit
Join AdaCore at Embedded Systems Summit
Event Details
- [In-Person]
- January 26 - January 28, 2027
- Silicon Valley, California
- Sonesta Silicon Valley
The Embedded Systems Summit returns for its second in-person edition. Built by embedded engineers for embedded engineers, the three-day event covers the technologies powering:
- IoT
- AI
- Robotics,
- Automotive,
- Medical
AdaCore will be attending the Embedded Systems Summit 2027.
Agenda
16:30 - 17:30, January 27th
Contracts Instead of Crashes: Proving a Bare-Metal I2C Driver with SPARK
A bare-metal driver checks arguments and state to catch incorrect use before it reaches the hardware. This talk shows how SPARK can move some of those checks to build time: express the driver's requirements as contracts, then prove that every caller satisfies them. Hardware errors still need run-time handling.
The example is a bare-metal I2C driver for the STM32F746, running in the Renode emulator against a BMP390 sensor. We walk through the original code, examine what the prover cannot establish, and make three changes that complete the proof. The central change is straightforward: replace a defensive check with a precondition, then verify the callers.
The result is every proof obligation discharged and the corresponding run-time checks removed. We explain what has been proved, what remains outside the proof, and how much work it took. We also compare SPARK's proof guarantees with Rust's safety guarantees, since both target the same class of bugs by different means.
Attendees will leave with a concrete example of applying contracts to a hardware abstraction layer, including the code changes and the reasoning behind them. No prior experience with SPARK or formal verification is assumed.