AI Meets Hoare Logic: Revolutionizing Software Testing with Formal Methods
Go beyond testing. Use AI and formal methods to mathematically prove your software is correct for all possible inputs.
#1about 3 minutes
The case for software verification in the AI era
AI-generated code is probabilistic and requires more than traditional testing, creating a need for formal software verification to ensure correctness.
#2about 3 minutes
Understanding the difference between testing and verification
Software testing finds errors through execution with selected inputs, while formal verification provides a complete mathematical proof of correctness for all inputs.
#3about 6 minutes
A primer on Hoare Logic and its core axioms
Hoare Logic uses preconditions, postconditions, and axioms like assignment and composition to formally prove that a piece of code behaves as specified.
#4about 1 minute
Current tools and applications for software verification
Modern verification relies on tools like SMT solvers and model checkers and is primarily used in critical systems like aerospace due to its high manual effort.
#5about 4 minutes
Verifying a binary search algorithm with OpenJML
A practical demonstration shows how to use OpenJML annotations like 'requires' and 'ensures' to formally verify a Java binary search implementation.
#6about 3 minutes
Using AI to generate formal verification proofs
AI tools like Gemini can generate verification annotations but may introduce subtle errors, highlighting the need for human oversight in this new validation workflow.
Related jobs
Jobs that call for the skills explored in this talk.
With AIs wide open - WeAreDevelopers at All Things Open 2025Last week our VP of Developer Relations, Chris Heilmann, flew to Raleigh, North Carolina to present at All Things Open . An excellent event he had spoken at a few times in the past and this being the “Lucky 13” edition, he didn’t hesitate to come and...
Benedikt Bischof
How we Build The Software of TomorrowWelcome to this issue of the WeAreDevelopers Live Talk series. This article recaps an interesting talk by Thomas Dohmke who introduced us to the future of AI – coding.This is how Thomas describes himself:I am the CEO of GitHub and drive the company’s...
Daniel Cranney
Panel Discussion: Responsible AI in Practice - Real-World Examples and ChallengesIntroductionIn the ever-evolving landscape of artificial intelligence, the concept of "responsible AI" has emerged as a cornerstone for ethical and practical AI implementation. During the WWC24 Panel discussion, three eminent experts—Mina, Bjorn Brin...
Chris Heilmann
Transforming Software Development: The Role of AI and Developer ToolsIn today's fast-paced tech landscape, AI has begun to play an increasingly significant role, reshaping the way developers create software. As we delve into this transformation, we uncover both opportunities and challenges that AI brings into the worl...
From learning to earning
Jobs that call for the skills explored in this talk.
27:54
45:24
31:39
28:09
25:14
15:26
04:17
31:56
