2026-06-15

[Caml-list] VSTTE 2026: Second Call for Papers and WIP Presentations

VSTTE 2026: Second Call for Papers and WIP Presentations

18th International Conference on Verified Software: Theories, Tools, and Experiments

14 September, 2026, Graz, Austria

Co-located with Formal Methods in Computer-Aided Design 2026 (FMCAD 2026)



Key Information


Important Dates:

Abstract submission: July 10th, 2026 AoE  July 17th, 2026 AoE
Paper submission: July 17th, 2026 AoE July 24th, 2026 AoE (firm, no further extensions)
Notification of acceptance: August 22nd, 2026 AoE (tentative)*
Final pre-conference paper submission (optional): September 2nd, 2026 AoE (tentative)
Camera-ready for papers included in post-conference proceedings: October 23, 2026 (tentative)

* Authors of accepted papers at VSTTE 2026 will be able to register at early-bird rates for FMCAD/VSTTE.


Paper Submissions:

VSTTE 2026 accepts both long (limited to 16 pages, excluding references) and
short (limited to 10 pages, excluding references) paper submissions. Short
submissions also cover “verification pearls” describing an elegant proof or
proof technique. Submitted research papers and system descriptions must be
original and not submitted for publication elsewhere.

Papers must be submitted via EasyChair at the VSTTE 2026 conference submission

The use of LaTeX and the Springer LNCS class files is strongly encouraged.

Submissions that are not in the proper format or are too long will not be considered.

Accepted regular-track papers will be included in the post-conference
proceedings of VSTTE 2026, which will be published as a LNCS volume by
Springer Verlag. Authors of those papers will have to transfer copyright of
their contribution to Springer Verlag.


Invited speakers
Invited tutorial

2026-06-10

[Caml-list] POPL 2027 Call for Workshops

POPL 2027 Call for Workshops
Sun 10 - Sat 16 January 2027
Mexico City, Mexico
https://popl27.sigplan.org/
=============================

Submission details

Deadline for submission: 24 July 2026

Notification of acceptance: 4 August 2026

A workshop proposal should provide the following information:

- Name of the workshop.
- A short description (150-200 words) of the workshop.
- Call for submissions.
- Duration of the workshop.
- Whether the workshop will be Conference-approved or SIGPLAN-approved (see below).
- Organizers: names, affiliation, contact information, brief (100 words) biography.
- Event format: workshop; type of submissions if any; review process; results dissemination.
- Expected attendance and target audience.
- Potential PC members - please do not contact them before the workshop is approved.
- History of the workshop.
- Plans for remote participation.

Please submit your proposals at
https://popl27.sigplan.org/track/POPL-2027-workshops-and-co-located-events

---------------------------------------------------------------------

SIGPLAN Sponsorship

POPL co-located events are sponsored by SIGPLAN (http://sigplan.org/).
There are two kinds of co-located events: Conference-approved (no
proceedings) and SIGPLAN-approved (proceedings in the ACM Digital
Library). See http://www.sigplan.org/Resources/Guidelines/Workshops/
for more information, including a full listing of prescriptions for
Conference-approved and SIGPLAN-approved workshops.

SIGPLAN-approved workshops must respect the SIGPLAN Diversity Policy.
Proposals for SIGPLAN-approved workshops must additionally include the
gender, country of affiliation, and professional status of potential
PC members. See https://www.sigplan.org/Resources/Policies/Diversity/
for more details.

---------------------------------------------------------------------

Selection committee

All submissions will be evaluated by a committee comprising the
workshops co-chairs, the general chair, and the program chair.

---------------------------------------------------------------------

Further information

Any questions regarding POPL 2027 co-located event proposals should be
addressed to the workshops chairs, Aws Albarghouthi (aws@cs.wisc.edu)
and Alan Schmitt (alan.schmitt@inria.fr).

2026-06-01

[Caml-list] PERR 2026 @ CAV/FLOC: Call for Participation

======================================================================
                        CALL FOR PARTICIPATION
       6th Workshop on Program Equivalence and Relational Reasoning
                24 July 2026 at ISCTE campus, Lisbon, Portugal
                  associated with CAV 2026 at FLOC 2026
                   https://perr-workshop.github.io/2026

======================================================================

PERR is an annual international workshop dedicated to the formal verification of program equivalence and related relational problems. It is the 6th in a series of meetings that bring together researchers from different areas interested in equivalence and related questions. PERR 2026 will be a workshop at FLOC 2026, and a satellite event to CAV 2026.

REGISTRATION

You can register for PERR 2026 here:


INVITED TALKS

- Cynthia Kop, Radboud Univeristy Nijmegen
- Thibault Dardinier, New York University

ACCEPTED PAPERS

- Differential Verification of Neural Networks: Theory and Applications by Samuel Teuber and Philipp Kern
- Interaction Equivalence by Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto and Gabriele Vanoni
- Process Equivalence Checking as Abstract Interpretation by Benjamin Bisping
- Proving Program Equivalence in Dafny by Nathaniel Victor, Dragana Milovancevic and Sophia Drossopoulou
- Refuting Equivalence in Probabilistic Programs with Conditioning by Krishnendu Chatterjee, Ehsan - Kafshdar Goharshady, Petr Novotný and Đorđe Žikelić
- Semantic Foundations for the Static Analysis of Program Revisions by Dakota Bryan and Bor-Yuh Evan Chang
- Semantically Descriptive Similarity by Oskar Hovmøller Dinesen and Christian Gram Kalhauge

PROGRAM COMMITTEE

Dragana Milovancevic (Co-chair), Imperial College London, UK
Mattias Ulbrich (Co-chair), Karlsruhe Institute of Technology, Germany
Andrzej Murawski, University of Oxford, UK
Carsten Fuhs, Birkbeck University of London, UK
Denys Shabalin, Google, Switzerland
Nikos Tzevelekos, Queen Mary University of London, UK
Ofer Strichman, Technion, Israel
Soumyadip Bandyopadhyay, ABB Corporate Research, India
Vasileios Koutavas, Trinity College Dublin, Ireland

2026-05-30

[Caml-list] APLAS 2026 SRC and Posters: Call for Papers (Wenjia Ye)

APLAS is of broad interest to the programming languages and TYPES communities,
including students working on type systems, type theory, formal semantics,
program analysis, verification, and related areas.

CALL FOR PAPERS

APLAS 2026 Student Research Competition and Posters
Co-located with APLAS & ATVA 2026
December 1-5, 2026

The APLAS 2026 SRC and Posters track invites submissions for its Student
Research Competition (SRC) and Posters track. This track provides an
interactive forum for researchers, practitioners, and students to present
work in progress, early-stage research, fresh ideas, and recent practical
systems or tool developments.

The track has two categories:

1. Student Research Competition (SRC)
Open to undergraduate and graduate students. Entrants will present their
work during the poster session. Selected finalists will then give a
presentation to compete for first, second, and third-place prizes.

2. Posters
Open to non-students, or students who do not wish to compete in the SRC.
Authors will present their work alongside SRC entrants during the main
poster session.

Submissions should fall within the scope of APLAS, including programming
languages and related areas.

Important Dates, AoE (UTC-12h)

- Submission deadline for extended abstracts: August 22, 2026
- Notification: September 26, 2026
- Submission deadline for posters and revised extended abstracts: November 7, 2026

Submission information:

Extended abstracts should be formatted using the acmart LaTeX template with
the options sigplan and review enabled, be no longer than 3 pages excluding
bibliography, and be submitted in PDF format via EasyChair.

For SRC submissions, the student should be the sole author. However, on the
EasyChair submission, supervisors should be listed as authors after the
student, so that reviewers and judges can identify conflicts of interest.

CFP:
https://conf.researchr.org/track/aplas-atva-2026/aplas-2026-src-posters

Submission link:
https://easychair.org/my/conference?conf=aplas2026srcposters

2026-05-29

[Caml-list] WPTE 2026 - Call for Participation - Rewriting Techniques for Program Transformations and Evaluation

WPTE 2026 (affiliated with FLoC 2026 in Lisbon, Portugal) 12th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (19 July 2026) Webpage: https://wpte2026.github.io/ --------------------------------------------------------------------------- The aim of WPTE is to bring together researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area. --------------------------------------------------------------------------- The workshop will have two invited talks, by: - Nada Amin, Harvard University - Nikos Tzevelekos, Queen Mary University of London (joint with GaLoP 2026) as well as six contributed presentations: - David B. Hulak, Arthur Freitas Ramos and Ruy J.G.B. de Queiroz: Sound Rewrites for Measurement-Bearing Expressions via Token-Sensitive Enclosure Semantics - Takumi Sato and Koji Nakazawa: A Cyclic Proof System for Trace Formula Implication with Least and Greatest Fixpoints - David Sabel and Manfred Schmidt-Schauß: Improvement Theory for Probabilistic Call-by-Need - Misaki Kojima and Naoki Nishida: On Comparing Python Programs Based on Differences in Rewrite Sequences to Support Grading Programming Exercises - Katarzyna Marek and Clément Pit Claudel: Tactic-driven code fusion - Ștefan Ciobâcă, K. Rustan M. Leino, Ștefan-Alexandru Mercas and Roxana-Mihaela Timon: An Interactive Proof Mode for Dafny Based on Back Translation of Verification Obligations --------------------------------------------------------------------------- Program Committee --------------------------------------------------------------------------- Martin Avanzini, Inria Sophia Antipolis Carsten Fuhs (co-chair), Birkbeck, University of London Jan-Christoph Kassing, RWTH Aachen University Thomas Kœhler, ICube Lab, CNRS, Université de Strasbourg Misaki Kojima, Nagoya University Rubén Rubio, Universidad Complutense de Madrid Traian Şerbănuţă, University of Bucharest Germán Vidal, Universitat Politècnica de València Janis Voigtländer (co-chair), University of Duisburg-Essen

[Caml-list] [CFP, Deadline Extension] HOPE'26: ACM SIGPLAN Workshop on Higher-Order Programming with Effect

Talk proposal deadline for HOPE 2026 is extended to Jun 12, 2026. Author notification will be on July 3, 2026. This year, the workshop will be co-located with ICFP'26 (Indiana, US) and FW'26 (Paris, France). ---------------------------------------------------------------------- HOPE 2026 The 14th ACM SIGPLAN Workshop on Higher-Order Programming with Effects August 24, 2026 (the day before ICFP 2026) https://icfp26.sigplan.org/home/hope-2026 HOPE 2026 aims to bring together researchers interested in the design, semantics, implementation, and verification of higher-order effectful programs. It will be*informal*, consisting of invited talks, contributed talks on work in progress, and open-ended discussion sessions. ---------------------- Call for Talk Proposals ----------------------- We solicit proposals for contributed talks. We recommend preparing proposals of at most 2 pages excluding references, in either plain text or PDF format. However, we will accept longer proposals or submissions to other conferences, under the understanding that PC members are only expected to read the first two pages of such longer submissions. When submitting talk proposals, authors should specify how long a talk the speaker wishes to give. By default, contributed talks will be 30 minutes long, but proposals for shorter or longer talks will also be considered. Speakers may also submit supplementary material (e.g. a full paper, talk slides) if they desire, which PC members are free (but not expected) to read. We are interested in talks on all topics related to the interaction of higher-order programming and computational effects. Talks about work in progress are particularly encouraged. If you have any questions about the relevance of a particular topic, please contact the PC chairs, Taro Sekiyama (tsekiyama@acm.org) and Francesco Gavazzo (francesco.gavazzo@unipd.it). Important Note: HOPE’26 will be co-located with ICFP’26 (https://icfp26.sigplan.org/) and FW’26 (https://www.irif.fr/~scherer/events/fpw-2026/announce.html). Presenters can choose either event to attend in-person. We also encourage remote participation and will support remote presentations. Deadline for talk proposals (extended): Jun 12, 2026 (Friday) Notification of acceptance (extended): Jul 3, 2026 (Friday) Workshop: August 24, 2026, Indiana, United States & Paris, France The submission website is now open: https://hope26.hotcrp.com --------------------- Workshop Organization --------------------- Program Committee: Yuyan Bao (Augusta University) Raphaëlle Crubillé (Aix-Marseille University) Francesco Dagnino (University of Genova) Elena di Lavore (University of Oxford) Francesco Gavazzo (University of Padua) Cristina Matache (University of Edinburgh) Ken Sakayori (The University of Tokyo) Taro Sekiyama (National Institute of Informatics) Dario Stein (Radboud University) Niels Voorneveld (Cybernetica) Zhixuan Yang (University of Exeter) --------------------- Goals of the Workshop --------------------- A recurring theme in many papers at ICFP, and in the research of many ICFP attendees, is the interaction of higher-order programming with various kinds of effects: storage effects, I/O, control effects, concurrency, etc. While effects are of critical importance in many applications, they also make code harder to build, maintain, and reason about. Higher-order languages (both functional and object-oriented) provide a variety of abstraction mechanisms to help “tame” or “encapsulate” effects (e.g. monads and handlers, ADTs, ownership types, typestate, first-class events, transactions, Hoare Type Theory, session types, substructural and region-based type systems), and a number of different semantic models and verification technologies have been developed in order to codify and exploit the benefits of this encapsulation (e.g. bisimulations, step-indexed Kripke logical relations, higher-order separation logic, game semantics, various modal logics). But there remain many open problems, and the field is highly active. The goal of the HOPE workshop is to bring researchers from a variety of different backgrounds and perspectives together to exchange new and exciting ideas concerning the design, semantics, implementation, and verification of higher-order effectful programs. We want HOPE to be as informal and interactive as possible. The program will thus involve a combination of invited talks, contributed talks about work in progress, and open-ended discussion sessions. There will be no published proceedings, but participants will be invited to submit working documents, talk slides, etc., to be made available online. -- Taro Sekiyama

[Caml-list] Summer School on Verification Technology, Systems & Applications

================================================================== First Call for Participation 14th International Summer School on Verification Technology, Systems & Applications http://www.mpi-inf.mpg.de/vtsa26/ The 18th edition of the Summer School on Verification Technology, Systems and Applications (VTSA) will be organized by the Max-Planck-Institute for Informatics Saarbruecken in cooperation with the University of Liege, Inria Nancy - Grand Est, and the University of Luxembourg. The school will take place from August 24 to August 28, 2026 on Saarland Informatics Campus, Saarbruecken, Germany. The following speakers have accepted to give courses at VTSA 2026: - Maria Paola Bonacina: Reasoning about Data Structures with CDSAT - Mathias Fleury: SAT Solving: 30 Years of CDCL, 20 Years of Proofs, 15 Years of Inprocessing, 3 Years of User Propagator - Mikoláš Janota: SMT Solving and Challenges and Opportunities - Cynthia Kop: Open-world Termination Analysis in a Small Functional Language - Christoph Scholl: Fully Automatic Formal Verification of Arithmetic Circuits Participation is free (except for travel and accommodation costs) and open to anybody holding at least a bachelor degree or equivalent in computer science. It includes the lectures, daily coffee breaks and lunches as well as a school dinner. Attendance is limited to 40 participants. Please apply electronically by sending an email to jmueller@mpi-inf.mpg.de: - a one-page CV, - an application letter explaining your interest in the school and your experience in the area, - a copy of your bachelor certificate (or equivalent or a more significant certificate), - a short statement if you want to contribute to the student sessions The deadline for application is July 5, 2026. Notification of acceptance will be given by July 10, 2026. Full details are available at http://www.mpi-inf.mpg.de/vtsa26/