ETAPS Industry Day 2025

From Software Engineering to AI Engineering: Bridging the Research-Industry Gap in the Age of Intelligent Systems

The software engineering landscape is undergoing a profound transformation as artificial intelligence evolves from specialized research to a fundamental industrial component. Just as software sciences required decades to achieve successful industrial adoption, we now face similar challenges translating cutting-edge AI research—particularly generative AI, large language models (LLMs), and emerging small language models (SLMs)—into production-ready solutions. Current trends reveal a critical disconnect: while LLMs demonstrate remarkable capabilities in code generation and automated testing, their industrial deployment faces barriers including computational constraints, reliability requirements, and integration complexity. Small language models offer pragmatic alternatives with reduced resource footprints, while emerging world models promise to revolutionize how AI systems understand and interact with complex environments, potentially transforming software verification and validation processes.

This keynote examines how lessons from decades of academic-industry collaboration in software sciences can accelerate AI technology adoption, addressing the gap between AI research breakthroughs and industrial implementation challenges. Looking toward the future, we envision AI-native software development where world models enable systems to simulate, predict, and optimize behavior across the entire lifecycle. However, realizing this vision requires intensive collaboration between researchers and practitioners to address practical constraints including safety, explainability, and regulatory compliance.

SPARK - Latest Industrial Challenges and Feature Development

SPARK is a formal proof tool for Ada programs that performs deductive verification. SPARK focuses on industrialization and usability by software developers (as opposed to strictly by proof experts). SPARK offers executable contracts that are part of the language, allowing mixed static/dynamic verification. SPARK also offers support for low-level features such as data representation in memory. In the last few years, SPARK has seen increased industrial adoption, in particular in embedded contexts. In this talk, we will present some of the latest challenges reported by industrial users of SPARK, as well as recent features that have been or are being introduced to address them and ease adoption.

Lean: A Unified Platform for Verification, Programming, and AI

Lean is an open-source programming language and proof assistant designed to bridge the gap between interactive and automated reasoning. In this talk, I provide an introduction to Lean and its distinctive features, including its expressive dependent type system, metaprogramming framework, and growing library of formalized mathematics. I then describe how AWS uses Lean across multiple domains: verifying Cedar (a policy language for access control) and SampCert (differential privacy primitives), implementing a tensor compiler, developing NeuroSymbolic AI systems, and building Strata, a uniform platform for language syntax and semantics. Finally, I discuss Lean’s central role in AI for mathematics, where it has become the foundation for systems achieving breakthrough results, from competition mathematics to open research problems, and is reshaping how mathematicians approach formalization and discovery.