CAV 2026 wrapup

As per last year, I wrote a summary of the Computer Aided Verification Conference (CAV2026) I attended in July. This summary usually serves as a basis for a presentation I give when coming back from the conference. It helps me to prioritize the papers to read and summarize, the people to contact and to make sense of what happened.

Highlights

Technical comments

Regarding Verification of Neural Networks, formal verification with absolute guarantees will only get you so far. Probabilistic guarantees (under the Provably Approximately Correct framework) is one of the new frontier to reach - exemplified by the work of ¹. Closed-loops systems with neural networks controllers are covered, as multiple case studies were presented at SAIV with controllers.

AI is more and more prominent in the tools we use - a vibe-coded verifier won the 2nd place at the VNN-COMP. Stanley Bak’s post, the author of that tool and of the prover nnenum, is insightful on the potential impacts it may have on our line of work². If our community wants to keep deliver what it’s good for - sound guarantees in software -, then trusting the formal methods tooling becomes a paramount endeavour. Proof certificates following the Alethe proof format³, certified decision procedures (akin to what was presented for Lean ⁴ and the work made for the Safety ONNX Profile ⁵) may thus become a priority for researchers.

Formal Explanation is building its niche, with a keynote from Guy Katz (in which my student’s work Jules Soria was featured) and work on object detection ⁶ is going under way. One question remains: what is the point of having formal explanations if we cannot assign meaning to the components of the explanation?

During his keynote, Leonardo de Moura said that “AI made Formal Verification Cost-Effective”. The irony of this wording does not removes its truth: if codeslop is to invade the world, formal verification have no other choice than to scale up.

Finally, with the rise of said “agentic AI”, composition of verification becomes a clear challenge for the community.

Papers

Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound

David Boetius, Stefan Leue, Tobias Sutter

Link to the paper

Probabilistic Verification is within our reach, by reusing existing branch and bound techniques. Altough scalability remains a question.

Automated Algorithm Configuration of alpha-beta-CROWN

Konstantin Kaulen, Holger H. Hoos

Link to the paper

Very nice contribution to the field. Automated configuration of provers allow to outperform most of previous entries in the VNN-COMP, even outperforming the authors' own configuration.

PICID: Proof-Driven Clause Learning in Neural Network Verification

Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, Guy Katz

Link to the paper

Conflict-Driven Clause Learning + Learning Clauses from Conflict Cause + Standard Proof format with Alethe = win.

Neural Network Verification using Partial Multi-Neuron Relaxation

Ido Shmuel, Guy Katz

Link to the paper

Verified Tensor Operators for Safety-Critical ML: From Specification to Reference Implementation

João Machado, Ricardo Silva, Loïc Correnson, João Galego, Eric Jenn, Hugo Daniel,Macedo Jean Souyris, Jorge Sousa Pinto

Non-technical comments

The conference venue was in an historical university. Altough it certainly helps by not having to rent a dedicated space, it also comes with some caveats. The conference coffee breaks were super noisy, which hampered proper communication. It made the whole conference more taxing than necessary, forcing me to skip sessions to go back to my place and take naps.

The food was served in a separated venue, in a buffet mode with AC and some tables. I believe this is the best way to have meaningful discussions during lunches, plus the catering was of good quality - there was at least one vegetarian option per meal and it was possible to have vegan options as well. Allergens were clearly displayed, which helped not to die when you are lactose intolerant.

Lisbon is a marvelous place to visit, but the lack of easy to access train lines makes it really hard to go there. I had to take the bus (48 hours, round-trip) which was also very tiring. I do not take the plane since 2018 for ecological reasons.

Tips for young researchers

Conferences are a crucial part for computer scientist career. They allow to keep up with the state-of-the-art by attending carefully crafted presentations of one’s last work. Gathering scientists is also a good way to foster collaborations. My PhD took place during the first COVID-19 pandemic. As such, all my publications at that time were given on remote - I started going to conferences on 2022, at IJCAI-ECAI. As a junior scientist, I struggled to interact with other people in my field, got really frustrated and tired of the experience. With retrospective, I believe it is because I did not had the opportunity to “learn the ropes” of the conference attitude.

By CAV 2026, things are different. I was invited at a Dagstuhl Seminar last year. I published several papers in high-ranking conferences. I am in a team developping actively a software used by industrial and academics, and I advise three PhD students. This newfound confidence helps me to identify which points I struggle when I start a community event - and trying to provide tips to people who may be in the same situation (and I believe there are quite some)

Strategize your focus

Energy and focus come in a limited quantity. Ensure to use it well.

I did not attended sessions where I did not know the authors nor understood the title. instead, I took time to discuss with colleagues and to keep my energy on the talks that mattered. The day before the conference, check the schedule and select the talks you will attend. Make sure you are following actively: use the best note-taking habit with you, try to come up with a question (hard!) and write it down or ask it.

If you are reading your emails or coding something else, there is a good chance that you could do that elsewhere and that the session is not beneficial for you.

Your mind is not an island

I am usually sensitive to what I call the “conference fever”. Meeting colleagues helps me to kickstart projects, writing drafts of papers and proposals. New ideas come when I attend to sessions and discussing with them. In other words: conferences are very stimulating. As such, I have the bad habit to overwork a lot. While it is sometimes expected and necessary to have longer work hours, especially as an academic, it is still important to set boundaries. Overstepping your limits will bite you back at some point.

Drink water - a lot (don’t drink only coffee!). Listen to your body. If you feel tired, then have naps. If you are upset or sad, go have a stroll or plan an afternoon with colleagues to visit the place.

Be seen is not impolite - it’s the goal

I was puzzled by the work “networking”. While I understood the general goal, I struggled to understand the actual tasks it yielded. Actively engaging interactions with people is a bit difficult for me, and I was afraid of being seen as rude or inconsequential (plus, the good old imposter syndrom was around the corner).

In reality, I believe that conferences are places where you are encouraged to shine and to be seen. It is a place to display your works, your achievements and your ideas. While socialization with fellow colleagues can feel intimidating - especially with people with seniority -, it is actually the expected behaviour. So don’t feel afraid to “plant flags”, as one of my former advisor said.

That said, here are some strategies and tools that I found helpful and may help your social endeavours:

• have an elevator speech, and have it ready. When presenting your work, you need to convey in a few sentences your research interest. It is your advisor’s role to help build this pitch
• if you are with other people of the lab, having a colleague (like your advisor) who is experienced and can handle introductions is a really nice help
• do not hesitate to ask for a schedule to present your work in further details, like a coffee break or a meal
• asking questions during the sessions can foster discussions during and after the session, as people will recognize you. Symmetrically, if somebody asked a question, you can go to them and start the interaction by mentioning that!
• a simple approach like asking for materials like tutorial I can bring back to your lab is a very good starter