Auto-Active Verification: The AutoProof Approach to Program Proofs

Speaker:  Bertrand Meyer – Zurich, Switzerland
Topic(s):  Human Computer Interaction , Artificial Intelligence, Machine Learning, Computer Vision, Natural language processing , Software Engineering and Programming , Computational Theory, Algorithms and Mathematics , Society and the Computing Profession , Applied Computing

Abstract

The "Grand Challenge" of verified software is to move beyond testing toward mathematical certainty. This lecture introduces AutoProof, a state-of-the-art static verifier for Eiffel that follows the "auto-active" paradigm. Unlike interactive provers that require constant human intervention, or fully automatic tools with limited scope, AutoProof allows developers to guide the proof process through source-code annotations (loop invariants, frame conditions, and contracts). The presentation details the tool’s internal pipeline: translating Eiffel into the Boogie intermediate language and utilizing SMT solvers (Z3) to discharge verification conditions. A key focus is on "Counterexample Extraction," a 2025-2026 advancement that converts failed proof attempts into executable tests, bridging the gap between formal proofs and practical debugging.

About this Lecture

Number of Slides:  30
Duration:  minutes
Languages Available:  English, French, German, Italian, Russian
Last Updated:  27/02/2026

Request this Lecture

To request this particular lecture, please complete this online form.

Request a Tour

To request a tour with this speaker, please complete this online form.

All requests will be sent to ACM headquarters for review.