[Deadline Extension] CfP: ACV Workshop at FLoC 2026

--000000000000f78b0a065130a64f
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

[Apologies for multiple postings]
************************************************************************
Call for Presentations

ACV 2026
--- First Workshop on Abstract and Concrete Techniques in Verification

https://acv-ws.github.io/2026/

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

Submission deadline: May 20th 2026 AoE (extended)
Organizers: Ichiro Hasuo, Bart Jacobs, Joost-Pieter Katoen, Sam Staton
************************************************************************

Highlights
-------------
- A new workshop, aiming to promote the unification of abstract and
concrete methods in formal verification
- Invited speakers: Mayuko Kori (RIMS, Kyoto U), Cristina Matache, (U
Birmingham), and many more

Workshop Scope
------------------------
Formal verification research stands upon two lines of work. One is on
abstract mathematical semantics of systems, defining systems=E2=80=99 behav=
iors
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=E2=80=94abstract and
concrete=E2=80=94have 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.


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 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
Submission link: https://submissions.floc26.org/acv/

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)

--000000000000f78b0a065130a64f
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">[Apologies for multiple postings]<br>*********************=
***************************************************<br>Call for Presentatio=
ns<br><br>ACV 2026<br>--- First Workshop on Abstract and Concrete Technique=
s in Verification<br><br><a href=3D"https://acv-ws.github.io/2026/" target=
=3D"_blank">https://acv-ws.github.io/2026/</a><br><br>At FLoC 2026, affilia=
ted with LICS 2026 and CAV 2026<br>Lisbon, Portugal, July 24-25, 2026<br><b=
r>Submission deadline: May 20th 2026 AoE (extended)<div>Organizers: Ichiro =
Hasuo, Bart Jacobs, Joost-Pieter Katoen, Sam Staton<br>********************=
****************************************************<br><br>Highlights<br>-=
------------<br>- A new workshop, aiming to promote the unification of abst=
ract and concrete methods in formal verification<br>- Invited speakers: May=
uko Kori (RIMS, Kyoto U),=C2=A0Cristina Matache, (U Birmingham), and many m=
ore<br><br>Workshop Scope<br>------------------------<br>Formal verificatio=
n research stands upon two lines of work. One is on abstract mathematical s=
emantics of systems, defining systems=E2=80=99 behaviors based on which for=
mal verification is conducted. The other one is on concrete algorithms and =
methods that enable efficient and scalable verification.<br><br>The two lin=
es have some marked differences in their ecosystems. For example, experimen=
tal evaluation is virtually a must for the latter, while it is not for the =
former. Their different orientations=E2=80=94abstract and concrete=E2=80=94=
have made them hard to communicate with each other.<br><br>However, a recen=
t 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 va=
lue of their abstract theory. Conversely, on the concrete side, abstraction=
, generalization, and unification of various concrete verification methods =
have been actively sought.<br><br>This way, a new form of unification of ab=
stract and concrete is emerging, centered around the mathematical languages=
 of lattices and categories. This also follows a well-beaten track of the s=
uccessful collaboration between abstract and concrete in programming langua=
ge research (such as monads in functional programming). Such unification is=
 much desired, too, now that the hard-to-(logically-)model nature of statis=
tical AI is posing methodological challenges to formal verification.<br><br=
>The goal of this workshop is to promote the unification of abstract and co=
ncrete and thus to incubate breakthroughs in formal verification. Specifica=
lly,<br><br>- we gather a wide audience from the formal verification commun=
ity,<br>- we share results, observations, and experience from both sides of=
 abstract and concrete,<br>- we seek a common language, and<br>- we seek ma=
tchings between abstract theories and concrete techniques,<br><br>Thereby p=
icturing a new form of formal verification research in the AI era.<br><br><=
br>Call for Presentations<br>-----------------------------<br>We solicit co=
ntributed presentations. Topics of interest include the following, although=
 the list is by no means exclusive.<br><br>- Abstract semantical techniques=
 in formal verification, towards concrete methods<br>=C2=A0 - Lattice-theor=
etic modeling<br>=C2=A0 - Categorical modeling<br>=C2=A0 - Algebras and coa=
lgebras<br>=C2=A0 - String diagrams<br>=C2=A0 - Implementation techniques f=
or abstract theories<br>- Concrete verification algorithms and methods, tow=
ards abstraction<br>=C2=A0 - Model checking<br>=C2=A0 - Theorem proving, au=
tomated and interactive<br>=C2=A0 - Program verification<br>=C2=A0 - Type s=
ystems<br>=C2=A0 - Probabilistic verification<br>=C2=A0 - Cyber-physical sy=
stems<br>=C2=A0 - Quantum systems<br>- Accessible introduction to basics, a=
bstract or concrete<br>=C2=A0 - Abstract semantical methods<br>=C2=A0 - Con=
crete verification methods<br>- Examples of successful matchings between ab=
stract and concrete, or efforts towards them<br><br>Submission<br>---------=
------<br>We call for presentation proposals describing ongoing research de=
velopments, an overview of past research, or a survey of a broad topic. A p=
resentation of already published results, or those currently under review, =
is welcome, too. There are no formal proceedings.<br><br>Submission deadlin=
e: May 6th 2026 AoE<br>Submission link:=C2=A0<a href=3D"https://submissions=
.floc26.org/acv/" target=3D"_blank">https://submissions.floc26.org/acv/</a>=
<br><br>Organizers<br>----------------<br>Ichiro Hasuo (National Institute =
of Informatics, Tokyo, Japan)<br>Bart Jacobs (Radboud University, Nijmegen,=
 the Netherlands)<br>Joost-Pieter Katoen (RWTH Aachen University, Germany)<=
br>Sam Staton (University of Oxford, UK)<div class=3D"gmail-yj6qo"></div><d=
iv class=3D"gmail-adL"><br></div><br class=3D"gmail-Apple-interchange-newli=
ne"></div></div>

--000000000000f78b0a065130a64f--