World Congress 2025 Aug 20, 2025 Session details

AI Meets Hoare Logic: Revolutionizing Software Testing with Formal Methods

Onur Kasimlar

Can mathematical proofs replace unit tests? AI makes it possible. Learn how Hoare logic and generative models shift your role from writing tests to validating mathematical certainty.

Pause
Mute Enter Fullscreen
#1 about 3 min

Raising awareness for software verification

How the rise of AI-generated code necessitates stronger validation methods than traditional software testing provides.

#2 about 3 min

Comparing software testing and software verification

The fundamental differences between detecting errors through execution and mathematically proving comprehensive code correctness.

#3 about 2 min

Fundamentals of Hoare logic

An introduction to Hoare logic using variables like preconditions, executable code steps, and postconditions.

#4 about 3 min

Applying Hoare logic axioms

How assignment, composition, and conditional axioms simplify complex software verification problems into solvable logical clauses.

#5 about 1 min

Backward reasoning in formal proofs

Working backward from desired postconditions to establish the required preconditions for verifying sequential programmatic statements.

#6 about 1 min

State of the art in software verification

How modern engineering teams apply formal methods, SMT solvers, and theorem provers to validate critical systems.

#7 about 5 min

Verifying Java code with OpenJML

A practical demonstration of annotating a Java binary search algorithm with OpenJML requirements and expected postconditions.

#8 about 3 min

Leveraging AI for code validation

Using generative AI tools like Gemini to automatically create verification annotations while monitoring constraints and false assumptions.

Matching moments

1:56 min

Managing AI speed and the rise of verification debt

Werner Vogels Werner Vogels +1 · World Congress 2026 Europe

1:51 min

Bridging the gap between AI code generation and verification

Christian Heilmann Christian Heilmann +3 · World Congress 2026 Europe

1:22 min

Overcoming initial skepticism of AI code generation

Jeff Blankenburg Jeff Blankenburg · World Congress 2026 Europe

3:01 min

Balancing artificial intelligence tools with foundational software engineering skills

Tim Ruscica · Coffee With Developers

2:12 min

The evolving role of software testing in AI development

Jakub Janczyk Jakub Janczyk · World Congress 2026 Europe

1:55 min

Verifying the quality of rapidly generated AI code

Krzysztof Cieślak Krzysztof Cieślak · World Congress 2026 Europe

Upcoming sessions on this topic

Open session

World Congress 2026 North America

September 24, 2026 · 15:30–16:00

Stage 5

The reviewer can't be the author: independent verification for AI-generated code

Manish Kapur

VP, Product and Solutions at Sonar

Manish Kapur
Open session

World Congress 2026 North America

September 25, 2026 · 11:40–12:10

Stage 2

Reinventing Testing Practices in the AI Era

Eric Deandrea

Java Champion & Senior Principal Software Engineer, IBM

Eric Deandrea
Open session

World Congress 2026 North America

September 24, 2026 · 16:50–17:20

Stage 6

Who Tests the AI? Building Trustworthy AI Systems at Enterprise Scale

Him Raj Singh

PayPal, Manager, Software Engineer

Him Raj Singh
Open session

World Congress 2026 North America

September 25, 2026 · 14:10–14:40

Stage 1

The Broken Rung: How AI is Rebuilding Software Development from the Ground Up

Tomislav Tipurić

Chief Technology Officer, Nephos

Tomislav Tipurić
Open session

World Congress 2026 North America

September 25, 2026 · 14:50–15:20

Stage 1

There's no dark factory without better software verifiers

Dexter Horthy

Co-Founder, HumanLayer

Dexter Horthy
Open session

World Congress 2026 North America

September 24, 2026 · 16:10–16:40

Outdoor Stage

When Humans Stop Writing Code: Rethinking Languages, Compilers, and Responsibility

Simon Auer

Organizer of flutter vienna meetup and CEO of marqably

Simon Auer