Fuzzing and Dynamic Analysis for High-Integrity Software with Paul Butcher

Fuzzing and Dynamic Analysis for High-Integrity Software with Paul Butcher We sit down with Paul Butcher, Unit Director of Dynamic Analysis at AdaCore, to explore verification techniques beyond basic compliance in safety-critical software. Paul shares his experience from Eurofighter to automated trains, explaining how dynamic analysis—from unit testing to coverage analysis to fuzzing—helps find bugs that traditional testing misses. The conversation dives deep into fuzzing: how it works, why it's so effective at finding corner-case bugs (even in well-tested systems), and the challenges of applying it to embedded systems with timing constraints. Paul introduces an intriguing approach that combines static analysis with targeted fuzzing to automatically triage false positives and generate reproducers. We also touch on formal verification, the role of LLMs in verification workflows, and why the simplest software is often the safest. Whether you're working in aerospace, medical devices, or any safety-critical domain, this episode offers practical insights into building more robust systems. Key Topics [02:30] Paul's background in high-integrity embedded systems: Eurofighter, rail, drones, and AdaCore's dynamic analysis tools [05:00] Dynamic vs. static analysis: executing code to observe real behavior across different environments [08:15] How fuzzing works: mutation engines, anomaly detection, and finding bugs through negative testing [14:20] Challenges of fuzzing timing and concurrency bugs in embedded systems [17:45] Real-world success: fuzzing the NH90 avionics via the MIL bus uncovered numerous bugs [22:30] Safety standards (DO-178C, SIL levels) and objective-based approaches vs. checkbox compliance [28:00] Determining 'enough' fuzzing: coverage, input space complexity, and building certification arguments [32:15] Combining static analysis with targeted fuzzing to automatically triage false positives and generate reproducers [38:45] Symbolic execution and theorem provers: breaking through complex branch conditions in fuzzing campaigns [42:00] Shift-left philosophy: building verifiable software from the start with testing and analysis tools [47:30] Formal verification in practice: London Underground's Victoria line uses SPARK-proven emergency braking [51:00] LLMs in verification: cautious adoption for report analysis, but determinism remains critical for core tools [54:30] High Integrity Software Conference (HISC) in Birmingham, October 2026 Notable Quotes "Software testing is typically about, is it functionally correct? Fuzzing is like a negative testing technique. It's the inverse of that. It fires random inputs into your system with the intent of finding anomalies." — Paul Butcher "Every time I speak to someone who's tried fuzzing, even if it's a system that's considered high integrity with a high level of assurance, they always find something. It's really good at eking out those weird corner case scenarios." — Paul Butcher "With testing you would like to prove the absence of bugs, but unfortunately you can't. So you have to settle for a very distant second place of proving the presence of bugs." — Luca Ingianni Resources Mentioned Paul's paper on fuzzing in safety-critical contexts - Detailed discussion of how to argue 'enough' fuzzing for certification High Integrity Software Conference (HISC) - Annual conference in Birmingham, UK (October 2026) covering high-integrity software across industries AdaCore Dynamic Analysis Tools - Coverage, fuzzing, and unit testing solutions for high-integrity software SPARK formal verification - Formal proof technology used in London Underground's Victoria line emergency braking AFL++ - Successor to the discontinued AFL (American Fuzzy Lop): Fuzzing technology mentioned as capable of quickly finding the Heartbleed bug You can find Jeff at https://jeffgable.com.You can find Luca at https://luca.engineer.Want to join the agile Embedded Slack? Click hereAre you looking for embedded-focused training