Embedded Executive LIVE
summary
A demonstrator called GNAT Foundry Intersection implements a traffic‑light controller in Ada with SPARK proof and proves absence of runtime errors, enforces V‑model traceability from concept of operations to code and generates code‑coverage, static analysis, formal proofs and test artifacts. An agentic AI workflow can request a feature (a countdown timer), produce code and a verification report; large frontier models handle the rules well while smaller open‑weight models often violate proofs. The build runs bare‑metal on STMicro F4/C5 and on Zephyr or QNX.
AI-written summary · about
related talks
02mexplains Ada's shrinking footprints
07mKeynote: Modernizing the Development of AI IoT Devices with WebAssembly-based...
20mDriving Intelligence: The Software Shift Shaping Tomorrow’s Cars
21mAPP4MC RaceCar: A Practical ADAS Demonstrator for Evaluating and Verifying Timing Behavior
47mEmbedded Systems Architecture
19mBoosting confidence in tiny AI deployment in embedded control systems
01h 05mAgile embedded development under regulatory constraints
01h 01mMicrocontrollers in Micro-increments...