wal.sh
home > events > pldi-2026 > page-2026 · Jun 15, 2026
agentic-engineeringformal-methodspldiverificationagent-safety

PAgE 2026: Principles of Agentic Engineering

Basics

Field Value
Date <2026-06-15 Mon>
Parent PLDI 2026, Boulder CO
Deadline 2026-05-06 AoE
Portal page2026.hotcrp.com
Recording PLDI 2026 Live Streams, Meadows B (Jun 15)
Contact sbarke@microsoft.com

Organizing committee

  • Shraddha Barke (Microsoft Research, Redmond)
  • Peli de Halleux (Microsoft Research)
  • Dan Grossman (University of Washington)
  • Madan Musuvathi (Microsoft Research)
  • Dawn Song (UC Berkeley)
  • Ben Zorn (Microsoft)

Submission tracks

  1. Archived papers (up to 10 pages) – published in ACM Digital Library
  2. Non-archival submissions (up to 6 pages) – work in progress, position papers, demos

Why PAgE matters

The PL community's formal-methods entry point into agent governance. The same territory BugBash approaches from the testing/DST side and ELS approaches from the Lisp/MOP side. The committee (Grossman, Song, Zorn) carries enough weight to set vocabulary that sticks.

Program (Mon 15 Jun 2026, Meadows B)

Chaired by Shraddha Barke. Two keynotes bracket two paper sessions.

Time Talk Who
09:10 Keynote: Formal Methods for Frontier AI Systems Gagandeep Singh (UIUC)
10:40 Agentic Code Reasoning Ugare, Chandra (Meta)
11:00 Towards Verified Code Reasoning by LLMs Sistla et al. (Google DeepMind)
11:20 Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code Rinard (MIT) [Remote]
11:40 The Next Frontier for AI-Generated Kernels: Correctness Martinez (MSR), Sorensen (UCSC)
12:00 Testing LLM-Generated Distributed Protocol Code Das, Coyne (Boston U.)
13:40 Combining Agentic AI and Lightweight Formal Methods to Find Bugs in a Production Hypervisor Katsura, Memarian, Sewell (Cambridge)
14:00 From Workarounds to Root Causes: Agentic Workflows on Browser GPU Compiler Stacks Ramesh, Levine, Sorensen (UCSC)
14:20 Event-based Design Abstractions for Agent Harnesses Becker, Ghavami, Zaiser, O'Donnell, Rinard, Tenenbaum, Mansinghka (MIT) [Recorded]
14:40 Lumos: Let there be Language Model System Certification Chaudhary et al. (UIUC) [Remote]
15:00 Lazy Validation and Self-Healing for Agentic Programs Tsampouris, Ioannidis, Symeonidis [Remote]
15:50 Keynote: Can Coding Agents Write Verifiably Correct Software? Shan Lu (Microsoft / UChicago) [Remote]

Accepted papers

Title Authors Pre-print
Agentic Code Reasoning Ugare, Chandra arXiv:2603.01896
Towards Verified Code Reasoning by LLMs Sistla, Balakrishnan, Rondon, Cambronero, Tufano, Chandra  
Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code Rinard  
The Next Frontier for AI-Generated Kernels: Correctness Martinez, Sorensen DOI, pre-print
Testing LLM-Generated Distributed Protocol Code Das, Coyne  
Combining Agentic AI and Lightweight Formal Methods to Find Bugs in a Production Hypervisor Katsura, Memarian, Sewell  
From Workarounds to Root Causes: Agentic Workflows on Browser GPU Compiler Stacks Ramesh, Levine, Sorensen  
Event-based Design Abstractions for Agent Harnesses Becker, Ghavami, Zaiser, O'Donnell, Rinard, Tenenbaum, Mansinghka  
Lumos: Let there be Language Model System Certification Chaudhary, Jain, Parhar, Sachdeva, Singh, Ranu, Singh arXiv:2512.02966
Lazy Validation and Self-Healing for Agentic Programs Tsampouris, Ioannidis, Symeonidis  

Connection to current research

Closest to the reversible-pipeline verification thread: Rinard's Axon verified compiler in Lean and Claude Code and the Cambridge lightweight formal methods + agentic AI hypervisor work – both the verification-first, agent-drives-the-prover pattern we used for the Lean Equiv and Dafny codec proofs. Shan Lu's closing keynote – can coding agents write verifiably correct software? – is the experiment those proofs run.

Related