Abstract: Mechanical program verification typically requires bridging the gap between conventional programming and the formal systems used for proving correctness. Interactive verification languages, such as Coq, demand manual proofs of correctness, while verification tools like Dafny rely on user-provided annotations to guide the verifier. Fully automated verification using SMT solvers eliminates the need for such input but diverges significantly from traditional programming paradigms. Meanwhile, model checkers explore all execution paths exhaustively but are constrained by the combinatorial explosion of state spaces, often limiting their analysis to bounded depths.
In this work, we propose a novel approach that combines classical interpretation with automated verification via SMT solvers. By embedding automated verification capabilities directly into a functional programming language, we demonstrate how this integration enables seamless reasoning about program correctness without sacrificing the familiarity of conventional programming constructs. Our methodology balances automation, expressiveness, and efficiency, paving the way for a unified framework that simplifies and accelerates the process of mechanical program verification.

Short bio: Prof. Dr. Christophe Scholliers heads the theory and practice of programming research lab (TOPL) at the Faculty of Sciences at Ghent University, Belgium. TOPL is dedicated to research in programming languages, partially driven by hardware innovations, investigating programming language abstractions and tools that might ease software development for new devices.