21st Workshop on Programming Languages and Analysis for Security (PLAS 2026)

Overview

PLAS explores the use of programming language and program analysis techniques to improve software security across compilers, machine learning models, and smart contracts. It promotes speculative, forward-looking ideas and insightful discussions at the intersection of programming languages and security.

Invited Speakers

Deepak Garg
Max Planck Institute for Software Systems

Towards robust verification of code compiled from unsafe languages

Abstract. In security practice, verified properties of a trusted component are only meaningful if they are robust, i.e., if they hold when the component is linked with arbitrary untrusted code. The standard way to establish a robust property of compiled code, as captured broadly in the area of compiler security, is to prove the property for the source program and show that the compiler robustly preserves it. However, for memory-unsafe languages like C, this approach is a non-starter: co-linked untrusted code, that we did not verify, can trigger undefined behavior, so the source program has no robust properties in the first place! Any security of the compiled code comes from the compiler, e.g., from hardening that turns out-of-bounds memory accesses into safe fail-stops. This talk presents a way to nonetheless verify such programs with reasoning at the source level. The key insight is to use a program logic whose proof rules follow the syntax of the source program, but whose soundness theorem speaks about the compiled program linked with arbitrary target-language code. The rules may therefore rely on guarantees that the source semantics does not provide but the hardening compiler enforces. To prove such a soundness theorem, we rely on DimSum, a multi-language semantic framework that models source programs, target programs and specifications as labeled transition systems. Generic linking and wrapping constructs in DimSum allow for modular proofs of soundness. The talk will cover the broad framework alongside one or two instances that start from a C-like language, compile to a capability architecture inspired by Cheri, with dedicated program logics designed to enforce robust safety or robust confidentiality properties.

Program

Abstracts are listed here.

Scope

• Side-channel vulnerability detection and elimination
• Verification techniques applied to adversarial learning and smart contracts
• Software isolation (e.g., SFI, sandboxing)
• Compiler/runtime-based hardening and monitoring
• Program analysis, binary analysis, and fuzzing
• Security enforcement mechanisms
• Cryptographic protocol verification
• Information flow and access control
• Security in web, IoT, and cloud programming languages

Submission Guidelines

We invite both short papers and long papers. For short papers, we especially encourage the submission of position papers that are likely to generate lively discussion as well as short papers covering ongoing and future work.

• Full papers: There is no page limit on long papers. Papers in this category are expected to have relatively mature content. Papers that present promising preliminary and exploratory work, or recently published work are particularly welcome in this category. Long papers may receive longer talk slots at the workshop than short papers, depending on the number of accepted submissions.
• Short papers: should be at most 2 pages long, plus as many pages as needed for references. Papers that present radical, open-ended and forward-looking ideas are particularly welcome in this category. Authors submitting papers in this category must prepend the phrase "Short Paper:" to the title of the submitted paper.

The workshop has no published workshop proceedings and there is no restriction on paper format other than the page limits stated above. Presenting a paper (either short or long) at the workshop does not preclude submission to or publication in other venues that are before, concurrent, or after the workshop. Papers presented at the workshop will be made available to workshop participants only.

Please submit your submissions (in PDF format) via the following website: https://plas26.hotcrp.com. We follow a single-blind reviewing process, so you do not need to anonymize your submissions.

Important Dates

Paper submission: June 20, 2026 AoE June 26, 2026 AoE

Author notification: August 7, 2026

Workshop date: November 19

Program Committee

• Gilles Barthe (Max Planck Institute for Security and Privacy, Germany)
• Dominique Devriese (KU Leuven, Belgium)
• Joshua Gancher (Northeastern University, USA)
• Roberto Guanciale (KTH, Sweden)
• Limin Jia (Carnegie Mellon University, USA)
• Adrien Koutsos (Inria Paris, France) (co-chair)
• Robert Künnemann (CISPA Helmholtz Center for Information Security, Germany)
• Hamed Nemati (KTH, Sweden) (co-chair)
• Marco Patrignani (University of Trento, Italy)

Previous Editions

• PLAS 2025: Taipei, Taiwan
• PLAS 2024: Salt Lake City, USA
• PLAS 2023: Copenhagen, Denmark
• PLAS 2022: Virtual
• PLAS 2021: Virtual
• PLAS 2020: Virtual
• PLAS 2019: London, UK
• PLAS 2018: Toronto, CA
• PLAS 2017: Dallas, TX, USA
• PLAS 2016: Vienna, Austria