Program Overview

Monday, 19 July

ACV

Workshop on Abstract and Concrete Techniques in Verification

Formal verification's abstract (semantical) and concrete (algorithmic) research lines have been hard to bridge. This workshop seeks to unify them through lattices and categories, toward formal verification for the AI era.

Organizers: Ichiro Hasuo, Bart Jacobs, Sam Staton

Monday, 19 July

FMAAI

Workshop on Formal Methods for Agentic AI

FMAAI brings together researchers and practitioners from formal methods, AI, and industry to explore how formal specifications, verification, and runtime enforcement can make autonomous AI agents safe and trustworthy. Topics include autoformalization of specifications and models, policy-based guardrails for agent actions, runtime verification and monitoring of agent behavior, inference of specifications from agent trajectories, and neurosymbolic approaches that combine LLMs with formal reasoning.

Organizers: Bettina Könighofer, Zvonomir Rakamaric, Hazem Torfah

Monday, 19 July

HYPER

Workshop on Hyperproperties: Advances in Theory and Applications

Hyperproperties capture specifications that relate multiple system executions, with applications ranging from secure software and hardware to cyber-physical and learning-enabled systems. HYPER 2027 brings together researchers from formal methods and its application domains to discuss recent advances and challenges in the specification, analysis, and application of hyperproperties.

Organizers: Tzu-Han Hsu, François Hublet, Ege Sarac, Clara Schneidewind

Monday, 19 July

POC

Principles of Certification Workshop

The Principles of Certification Workshop provides a forum for the researchers and practitioners from different formal methods communities that work on certification of computing systems, including software and hardware verification, SAT and SMT solving, probabilistic system verification and verification of AI-enabled systems. The goal of certification is not only to formally prove that a model satisfies a specification, but also to provide the user with a certificate, which serves as a witness of correct verification and thus enhances the trustworthiness of formal verification results and tools.

Organizers: Emily Yu, Djordje Zikelic

Monday, 19 July – Tuesday, 20 July

SMT

Workshop on Satisfiability Modulo Theories

Satisfiability Modulo Theories (SMT) solving means combining decision procedures with propositional satisfiability solvers in novel ways to solve challenging problems from domains ranging from software verification to scheduling. The SMT workshop brings together researchers and users of SMT tools and techniques to nurture this development.

Organizers: Katalin Fazekas, Hans-Jörg Schurr

Monday, 19 July

VQC

Workshop on Verification of Quantum Computing

The Second Workshop on Verification of Quantum Computing (VQC 2027) brings together researchers in formal methods and quantum computing to advance the verification of quantum software and hardware. For CAV researchers, the workshop offers an opportunity to bring their verification expertise to quantum computing, discover challenging new problems, and connect with potential collaborators.

Organizers: Yu-Fang Chen, Alfons Laarman, Runzhou Tao

Tuesday, 20 July

CREST

Workshop on Formal Reasoning about Causation, Responsibility, and Explanations in Science and Technology

CREST is a forum for formal reasoning about causation, responsibility, and explanation in computing systems, covering topics from causal logics and actual causality to explainability, accountability, and fault ascription. It brings together researchers from different communities to discuss recent results, tools, and applications.

Organizers: Hadar Frenkel, Caroline Lemke

Tuesday, 20 July

FORCE

Formal Reasoning for Compositional Systems Engineering

The goal of the FORCE workshop is to bring together scientists and industry to harness in complex systems engineering the wealth of theories and tools that have been developed for compositional co-design and formal reasoning about digital hardware and software systems. We aim to explore theory, methodologies, and tools to formally prove properties of complex systems that require a multi-disciplinary approach, and study a variety of complex systems through the lens of formal methods.

Organizers: Alessandro Cimatti, Paula Herber, Inigo Incer

Tuesday, 20 July

SYNT

Workshop on Synthesis

Organizers: Anand Balakrishnan, Bettina Könighofer, Doron Peled

Website to be announced.

Tuesday, 20 July

VeriProP

Workshop on Verification of Probabilistic Programs

VeriProP 2027 brings together researchers interested in the tool-supported verification of probabilistic programs, models, and systems. The workshop provides a forum for presenting ongoing and previously published research, with a particular focus on symbolic methods and compositional approaches.

Organizers: Christoph Matheja, Francesca Randone, Fabian Zaiser

Tuesday, 20 July

VMW

Mentoring Workshop

Website to be announced.