PAgE 2026
| title | author | length |
|---|---|---|
| Towards Verified Code Reasoning by LLMs | Meghana Aparna Sistla, Gogul Balakrishnan, Pat Rondon, José Pablo Cambronero, Michele Tufano, Satish Chandra | 22m |
Builds a pipeline that extracts an LLM’s code reasoning as predicates via an LLM-based formalizer, encodes code semantics and a verification condition in… | ||
| The Next Frontier for AI-Generated Kernels: Correctness | Guido Martínez, Tyler Sorensen | 29m |
KernelBench’s fixed test suites let buggy kernels pass tests and even reject correct implementations; mutation testing finds racey softmaxes and trivial… | ||
| Formal Methods for Frontier AI Systems | Gagandeep Singh | 01h 08m |
Claims a concrete verifier that computes the probability mass of unsafe outputs for a single prompt (not just samples), implements a token-tree/ frontier… | ||
| From Workarounds to Root Causes: Experience Using Agentic Workflows to Debug Complex(…) | Abhijit Ramesh, Reese Levine, Tyler Sorensen | 18m |
Porting llama.cpp to the browser via WebGPU exposes a bug chain across WGSL, browser runtimes, compiler rewrites, and Metal; a context-managed, re-steerable… | ||
| Lumos: Let there be Language Model System Certification | Isha Chaudhary, Vedaant Jain, Prineet Parhar, Kavya Sachdeva, Avaljot Singh, Sayan Ranu, Gagandeep Singh | 21m |
Lumos is a domain-specific language that encodes prompt distributions as text-rich graphs, samples random subgraphs via a subgraph sampling operator, templates… | ||
| Lazy Validation and Self-Healing for Agentic Programs | Theodoros Tsampouris, Eleftherios Ioannidis, Andreas Symeonidis | 21m |
A typed DSL called Pact DSL treats LLM plans as programs, with generated JSON-schema types, workflows, and access-control policies validated at the point of… | ||
| Testing LLM-Generated Distributed Protocol Code | Brendan Coyne, Ankush Das | 13m |
Testing LLM-Generated Distributed Protocol Code (Video, PAgE 2026)
Brendan Coyne, Ankush Das
(Boston University, USA; Boston University, USA)
Abstract: Large… | ||
| Event-based Design Abstractions for Agent Harnesses | McCoy R. Becker, Matin Ghavami, Fabian Zaiser, Timothy J. O'Donnell, Martin C. Rinard, Joshua B. Tenenbaum, Vikash K. Mansinghka | 18m |
Proposes an event-driven harness where a durable append-only event log is the single source of truth, with independent facets that fold over the log to derive… | ||
| Opening remarks | Shraddha Barke | 04m |
Workshop defines an agent program as prompts, tool calls, memory, dynamic traces and highlights concrete challenges: traces that run for thousands of tool… | ||
| Combining Agentic AI and Lightweight Formal Methods To Find Bugs in a Production(…) | Hiroyuki Katsura, Kayvan Memarian, Peter Sewell | 22m |
Combines the executable-spec framework for Android pKVM with an OpenAI Codex-based agent that writes ambient-C ghost code and tests, running for about one… | ||
| nothing matches | ||