Worshop Sponsor
The VERIFAI workshop, sponsored by CNRS, is the first of its kind. It is devoted to the interplay between the two technologies: not only how to verify AI tools but also (the main focus) how verification techniques can make “vibe coding” efficient and reliable.
The workshop has now successfully ended. Everyone is working on preparing their articles for publication in Springer Lecture Notes in Computer Science (LNCS).
Topics
Topics of interest include, but are not limited to:
- Using verification and validation techniques to filter, control and certify AI-produced software.
- Using AI to generate and validate both implementations and specifications
- Analyses of the quality of AI-generated software and vibe coding.
- Using AI to generate and run proofs and other static analyses.
- Using AI to generate and run tests.
- AI-based verification tools.
- Using AI for software engineering tasks other than coding: vibe requirements, vibe specification, vibe contracting, vibe design, vibe testing, vibe verifying…
- The hallucination phenomenon and how to deal with it.
- Empirical studies of properties of AI-supported software.
- Experience reports in academia and industry.
- Verifying AI systems.
The word “verification” in the title of the VERIFAI workshop should be understood in a broad sense, including “validation” (“V & V”) and a wide range of software analysis techniques, from proofs to tests.
Empirical analyses providing quantitative assessments of the use of AI to produce software are particularly welcome.
Program committee
- Saddek Bensalem (University of Grenoble-Alpes, France)
- Amel Bennaceur (Open University, UK)
- Silvia Bonfanti (University of Bergamo, Italy)
- Jean-Michel Bruel (University of Toulouse, France)
- Swarat Chaudhuri (University of Texas, USA)
- Benoît Combemale (INRIA, France)
- Sophie Ebersold (University of Toulouse, France)
- Angelo Gargantini (University of Bergamo, Italy)
- Li Huang (Constructor Institute of Technology, Switzerland)
- Mikoláš Janota (Czech Technical University, Prague)
- Guy Katz (Hebrew University, Israel)
- Atif Mashkoor (Johannes Kepler University, Austria)
- Tim Menzies (North Carolina State University, USA)
- Bertrand Meyer (Eiffel Software, USA/Switzerland)
- Rosemary Monahan (Maynooth University, Ireland)
- Gail Murphy (University of British Columbia, Canada)
- Ileana Ober (University of Toulouse)
- Iulian Ober (ISAE (Institute of Space Technology), France)
- Iulian Neamtiu (New Jersey Institute of Technology, USA)
- Omer Landry Nguena Timo (Université du Québec en Outaouais, Canada)
- Manuel Oriol (Constructor Institute of Technology, Switzerland)
- Meriem Ouederni (University of Toulouse, France)
- Cesare Pautasso (University of Lugano, Switzerland)
- Bernard Steffen (TU Dortmund, Germany)
- Xingyu Zhiao (University of Warwick, UK)
About the workshop
The workshop is to help improve the state of the art and realize the full potential of using AI to generate high-quality software reliably and effectively.
The focus is on interaction between the participants. They will have access to each other’s papers ahead of the meeting and are encouraged to read them in advance. In addition to presentation sessions, ample time has been set aside for discussions and joint work.
Conference chair
Bertrand Meyer (Eiffel Software)
Program chairs
- Jean Michel Bruel (University of Toulouse)
- Bertrand Meyer (Eiffel Software)
Accepted papers
For the most up-to-date information and the schedule of presentations see the program page.
Mateen Abbasi, Petri Ihantola, Tommi Mikkonen and Niko Mäkitalo: Validating Multi-Model AI-Generated Acceptance Criteria in Requirements Engineering
Maryam Assmar, Alain Giorgetti, Meriem Ouederni and Sylvie Trouilhet: Challenges for Engagement between Software Engineering and Artificial Intelligence
Arshad Beg, Diarmuid O’Donoghue and Rosemary Monahan: Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics
Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini and Nico Pellegrinelli: Formalizing and validating properties in Asmeta with Large Language Models
Jessy Colonval, Fabrice Bouquet, Lefevre Louis, Antoine Perrotin, Éléa Jacquin and Frédéric Dadeau: Automatic Generation of Executable Script from MBT Scenario
Maxence Demougeot, Sylvie Trouilhet and Jean-Paul Arcangeli: Adaptive Random Testing of Online Machine Learning Programs: Application to Opportunistic Software Composition
Armel Fedoung Sanou, Badr Youakim and Fabrice Mourlin: Modeling and Analysis of Non-Deterministic Executions of LLM-Based Agents via Finite Automata
Thomas Flinkow and Rosemary Monahan: Machine Learning with Verifiable Guarantees
Leonel Gamvou Taklai, Jonathan Roy, Fehmi Jaafar and Sylvain Hallé: Trustworthy Machine Learning Across the Lifecycle: A Synthesis of Current Methods
Gabriela Gonzalez-Saez, Yves Ledru and Nicolas Hili: Towards an Evaluation of LLM’s Prior Knowledge for Test Case Generation
Li Huang, Ilgiz Mustafin, Alessandro Schena, Marco Piccioni, Bertrand Meyer and Reto Weber: Do AI models help produce verified bug fixes?
Muhammad Khalid and Oriol Manuel: ReqFusion: A Multi-Provider Framework for Automated PEGS Analysis Across Software Domains
Kalvin Thuan-Phong Khuu, Andrew Bovbel, Nirmal Chaudhari, Baptiste Lacroix, Richard Paige and Sebastien Mosser: Lightweight Safety Modelling to Support the Validation of Machine Learning Pipelines
Mahwish Kundi, Faraz Ahmad and Rosemary Monahan: FrameLLM for Requirements Generation: A Framework for Reducing Prompt Dependency and Improving Requirement Clarity and Completeness
Yves Ledru, Gabriela Gonzalez-Saez and Nicolas Hili: Challenges of using LLMs for software testing
Tatiana Liakh, Polina Ovsiannikova and Bianca Wiesmayr: Validating LLM-based Repair Agents for Distributed Control Software via Fault Injection and Formal Verification
Enrico Lipparini and Massimo Bartoletti: Certified LLM-produced counterexamples for smart contract verification
Tim Menzies and Kishan Ganguly: From Verification to Herding: Exploiting Software’s Sparsity of Influence
Maha Moujahed, Meriem Ouederni and Souheil El Alimi: Verified Vibe Coding in Energy Management: Runtime STL Monitoring of Battery Dispatch Strategies
Logan Murphy, Aren A. Babikian and Marsha Chechik: Abductive Vibe Coding
Iulian Ober, Ileana Ober and Anca-Miruna Constantin: AI-augmented MBSE: from vibe-modeling to assisted verification and validation
Liam O’Reilly, Filippos Pantekis, Alma Rahat, Markus Roggenbach and Mukesh Tiwari: An Emperical Study on Generating Proven-to-be-Correct Dafny Programs
Cesare Pautasso: On the Paradox of Generative Reuse
Laura Plein, Alexi Turcotte, Arina Hallemans and Andreas Zeller: Synthesizing Realistic Test Data without~Breaking~Privacy
Ocan Sankur, Thierry Jéron, Nicolas Markey, David Mentré and Reiya Noguchi: Requirement-Based Testing: Enhancing Reinforcement Learning with Game Theory
Alessandro Schena, Ilgiz Mustafin and Julia Kotovich: Large Language Models and Language Server Protocol: a match made in context
Dorine Tabary, Eléa Jacquin, Fabrice Bouquet and Frédéric Dadeau: Automated evaluation of test requirements generation with LLMs
Shirley Yu and Ruben Martins: Diversifying to Verify: When Equivalent Programs Differ in Verifiability
Sol Zilberman and Betty Cheng: Probabilistic Behavior Synthesis with Language Models for Autonomous Vehicle Testing
Dmitrii Zorin: Solver-Backed Traceable Consistency Checking of Index Methodologies: A Pilot Study
Program outline
See the program page.
Contact
To contact the organizers, you may write to villebrumier at fastmail dot fm (click the preceding link for a mail client window).