ACV 2026

ACV 2026

First Workshop on Abstract and Concrete Techniques in Verification

July 24-25, 2026
At FLoC 2026, affiliated with LICS 2026 and CAV 2026
Lisbon, Portugal

Workshop Scope

Formal verification research stands upon two lines of work. One is on abstract mathematical semantics of systems, defining systems’ behaviors based on which formal verification is conducted. The other one is on concrete algorithms and methods that enable efficient and scalable verification.

The two lines have some marked differences in their ecosystems. For example, experimental evaluation is virtually a must for the latter, while it is not for the former. Their different orientations—abstract and concrete—have made them hard to communicate with each other.

However, a recent scientific trend points to the need, feasibility, and prolificacy of the unification of abstract and concrete. On the abstract side, more works have implementations and experiments, demonstrating right away the practical value of their abstract theory. Conversely, on the concrete side, abstraction, generalization, and unification of various concrete verification methods have been actively sought.

This way, a new form of unification of abstract and concrete is emerging, centered around the mathematical languages of lattices and categories. This also follows a well-beaten track of the successful collaboration between abstract and concrete in programming language research (such as monads in functional programming). Such unification is much desired, too, now that the hard-to-(logically-)model nature of statistical AI is posing methodological challenges to formal verification.

The goal of this workshop is to promote the unification of abstract and concrete and thus to incubate breakthroughs in formal verification. Specifically,

  • we gather a wide audience from the formal verification community,
  • we share results, observations, and experience from both sides of abstract and concrete,
  • we seek a common language, and
  • we seek matchings between abstract theories and concrete techniques,

thereby picturing a new form of formal verification research in the AI era.

Invited Speakers:

  • Syyeda Zainab Fatmi, U Oxford, UK
  • Benjamin Kaminski, Saarland University, Saarbrücken, Germany & U College London, UK
  • Mayuko Kori, RIMS, Kyoto U, Japan

  • Cristina Matache, U Birmingham, UK

    An equational axiomatization of dynamic threads
    Algebraic effects are a way to describe and reason about computational effects in a modular way, via the algebraic theories from universal algebra. A current challenge is to extend these ideas to concurrent programming. In this talk, I will present recent work on modelling dynamic thread creation, inspired by POSIX fork, using an algebraic theory. The main result characterizes this algebraic theory in terms of labelled partial orders, leading to a semantics where concurrent programs denote partial orders. The algebraic theory provides sound and complete equational reasoning principles for equality of such partial orders. This is joint work with Ohad Kammar, Jack Liell-Cock, Sam Lindley, and Sam Staton.

  • Florian Wittbold, U Duisburg-Essen, Germany

… more are TBA

Contributed Presentations:

Each slot is (20-min talk + 10-min discussion), to bridge different backgrounds.

Program: TBA

Call for Presentations

We solicit contributed presentations. Topics of interest include the following, although the list is by no means exclusive.

  • Abstract semantical techniques in formal verification, towards concrete methods
    • Lattice-theoretic modeling
    • Categorical modeling
    • Algebras and coalgebras
    • String diagrams
    • Implementation techniques for abstract theories
  • Concrete verification algorithms and methods, towards abstraction
    • Model checking
    • Theorem proving, automated and interactive
    • Program verification
    • Type systems
    • Probabilistic verification
    • Cyber-physical systems
    • Quantum systems
  • Accessible introduction to basics, abstract or concrete
    • Abstract semantical methods
    • Concrete verification methods
  • Examples of successful matchings between abstract and concrete, or efforts towards them

Submission

We call for presentation proposals (typically 1-2 pages) describing ongoing research developments, an overview of past research, or a survey of a broad topic. A presentation of already published results, or those currently under review, is welcome, too. There are no formal proceedings.

Submission deadline:   May 6th 2026 AoE   May 20th 2026 AoE (extended)
Submission link: https://submissions.floc26.org/acv/
Notification: late May 2026 (before the early workshop registration deadline)

Attending

The workshop takes place on July 24-25, 2026, at FLoC 2026.

Organizers

Ichiro Hasuo (National Institute of Informatics, Tokyo, Japan)
Bart Jacobs (Radboud University, Nijmegen, the Netherlands)
Joost-Pieter Katoen (RWTH Aachen University, Germany)
Sam Staton (University of Oxford, UK)

Acknowledgments

Many thanks are due to the FLoC 2026 organization team. The workshop is partially supported by JST ASPIRE Grant No. JPMJAP2301.