Call for Papers: Unsound - Sources of Unsoundness in Verification (Deadline Extension: 2022-09-16)

Skip to first unread message

Jan Bessai

Sep 2, 2022, 4:43:21 PM9/2/22
to Jan_Bessai,,,,,,,,,,,,
Call for Papers

1st Workshop on Sources of Unsoundness in Verification
at SPLASH 2022

Software and proof verification has grown significantly in the last 15
Growth has come to the point where verification systems are complex and
manually proving the soundness of those verification systems sometimes
exceeds what a single research group can understand and verify as

Even formally defining soundness can be challenging and its definition
is varying from system to system. Specific research groups can have very
specific notions of soundness they focus on, but those can diverge from
what the users expect, especially if the users come from a different
verification environment or they are approaching verification for the
first time.

Participants to Unsound will be able to share their experience and
exploits on how different verification tools can either be broken or
expose confusing behavior, likely to be unexpected by users.
We think this would be greatly beneficial not only because it will help
all of us to iron out those unsoundnesses but also because it will
facilitate understanding of the foundational differences between the
assumptions of the various research lines.

The current academic environment encourages us to talk about the success
case of our work. In this workshop we want to address and learn from
failure cases and we want to reinforce the bedrock of our understanding.
In practice, when we divert our focus to a specific aspect of
we may (understandably) be less precise.
For example, a line of research focusing on aliasing control in OO may
be less precise when considering the implication in other areas, like
We believe that learning from the issues of many verification projects
can broaden the attention of researchers to topics which so far escaped
their focused area of research; e.g., from only type correctness to also
avoiding stack overflows.

We believe that this environment would be particularly beneficial for
young researchers that are in search of open questions in verification.
This may provide a motivation to deep dive into the details of any
particular tool, or to expand their individual area of expertise to get
a wider and more objective and critical view of the whole area of

We also wonder if in our fast expansion we accidentally glossed over
some fundamental issue in verification, and if our mistake has now
become engraved into the established wisdom and it is sometimes
uncritically assumed as a valid reasoning stepping stone.

We are particularly interested in sources of unsoundness that are
accidentally shared by many different unrelated research lines, and to
develop an understanding on why this is the case.

The workshop would be its first instance and is meant to be welcoming
for both people with strong theoretical skills, as well as people who
just like hacking things. We do not expect fully polished submissions
and we will not have formal proceedings. Students are especially welcome
to attend.

### Examples for possible contributions would be:

* Definition of sound and unsound and how they can diverge between
* Divergences between user assumptions and actual definitions of
* Common sources of unsoundness and why they emerge.
* Bugs and unsoundnesses in the process of extracting a concrete program
from a verified environment, e.g., from Coq to Haskell.
* Logic errors in the specification of a verification tool, e.g.,
* Bugs in the implementation of proof checkers.
* Overconfident generalizations of sound subsystems to larger settings,
e.g., imperative techniques in OO settings.
* Disproving soundness statements in published papers about
* Finding statements proven in published literature that should no
longer be trusted because they relied on a broken verification system.
* Simply proving False in a verification tool, in particular we are
interested in practical ways to trick available tools to accept wrong
* Breaking reasoning about programs with types by breaking the type
system of the programming language in new and interesting ways.
* Bad interactions between axiomatic choices in libraries used in
* Impacts of the false sense of security when the chain of trust is
broken by
subtle unsoundness in verification tools.

### Contributions:

*Extended Deadline: 2022-09-16 (23:59 AOE)*
Submissions should have 3 pages of text. Additional material
(bibliography, related work, and code examples) will not count toward
this limit.
We strongly encourage authors to include instructions to reproduce
results or exploits.

There will be a friendly peer review process, focusing on checking that
the submitted material is appropriate for the workshop.

#### Publication
Informal proceedings will be made publicly available on the workshop web
page. However, presentation at Unsound does not count as prior
publication, and can later be published at a conference of the authors'

### Instruction to Authors

#### Submission

Authors should be aware of ACM’s policies on plagiarism

Program Committee members are allowed to submit papers.

Papers must be submitted online at:

#### Formatting:

Submitted papers should be in portable document format (PDF), formatted
using the ACM SIGPLAN style guidelines. Authors should use the acmart
format, with the acmsmall sub-format for ACM proceedings. For details,

It is recommended to use the review option when submitting a paper; this
option enables line numbers for easy reference in reviews.
Reply all
Reply to author
0 new messages