The widespread adoption of language models for code generation makes the enforcement of formal guarantees on their outputs ever more important. Recent constrained decoding techniques are promising, but when applied to practical programming languages they typically face a trade-off between soundness and completeness, either permitting some invalid programs or rejecting some valid ones. We argue that invalid programs should be excluded entirely, yet find that overly restrictive acceptance criteria can significantly impair a model’s ability to follow human intent and generate functionally correct code. We attribute this degradation to a mismatch between the model’s internal representation of the language and the constrained language induced by the formal guarantees. To better align the two, we propose reducing variability through training-set preprocessing, language design, or neural architecture design.

Wed 17 Jun

Displayed time zone: Mountain Time (US & Canada) change

17:50 - 19:30
PLDI Reception with Student Research Competition PostersStudent Research Competition at The Lawn

Reception for all attendees with light refreshments and Student Research Competition posters.

17:50
1h40m
Talk
K-Sentry: A Verified Order-Sensitive Telemetry Accumulator
Student Research Competition
Sudrit Ghimire Texas State University
File Attached
17:50
1h40m
Talk
Smocq: Formal Verification of Self Modifying Code
Student Research Competition
Ilan Buzzetti University of Texas at Dallas
File Attached
17:50
1h40m
Talk
Formal Methods for Securing Federated Authorization: A Case Study of SciTokens
Student Research Competition
Minh Le Georgia Institute of Technology
17:50
1h40m
Talk
Scenario-based Proof for Distributed Protocols
Student Research Competition
Zhendong Ang National University of Singapore
File Attached
17:50
1h40m
Talk
Language Models Need Some Space: On the Sensitivity of Constrained Decoding to Completeness
Student Research Competition
Jahrim Gabriele Cesario University of St. Gallen
Link to publication File Attached
17:50
1h40m
Talk
Formal Proofs of Bit Hacks in Machine Code
Student Research Competition
Humam Alhusaini University of Texas at Arlington
File Attached
17:50
1h40m
Talk
LLMEffect: A Type System for Securing LLM API Boundaries
Student Research Competition
Sanjib Kumar Sen Texas A&M University - Corpus Christi
File Attached
17:50
1h40m
Talk
Pync: Function-Level Incremental Execution for Python Scripts
Student Research Competition
Bolun Thompson University of California, Los Angeles
File Attached
17:50
1h40m
Talk
Correctly Rounded Dot Products under Round-to-Odd
Student Research Competition
Sehyeok Park Rutgers University
File Attached
17:50
1h40m
Talk
Impulse: Momentously Fast, General, and Portable Probabilistic Programming via Compiler Augmentation
Student Research Competition
Siyuan Brant Qian University of Illinois at Urbana-Champaign
File Attached
17:50
1h40m
Talk
Towards Taming Indirect Control Flow in Binaries with Multi-Task Graph Learning
Student Research Competition
Kun Liu Tulane University
File Attached
17:50
1h40m
Talk
CAST: Continuous Fuzzing for SMT Solvers
Student Research Competition
Andrei Zhukov ETH Zürich
File Attached
17:50
1h40m
Talk
Implementing Hybrid Resource Analysis in Resource Aware ML 2
Student Research Competition
Arnav Sabharwal Carnegie Mellon University
File Attached
17:50
1h40m
Talk
Modular Verification of Leakage Contracts
Student Research Competition
Aditya Ranjan Jha National University of Singapore
File Attached
17:50
1h40m
Talk
Cumulating Abstract Semantics via Handlers
Student Research Competition
Cade Lueker University of Colorado Boulder
File Attached
17:50
1h40m
Talk
Semantics Lifting for Scientific Kernels
Student Research Competition
Naifeng Zhang Carnegie Mellon University
File Attached
17:50
1h40m
Talk
pp-horn: A Secure Inference Primitive
Student Research Competition
Sai Lalith Kumar Aka University of Colorado Boulder
File Attached
17:50
1h40m
Talk
Automatic Energy Analysis Using Types
Student Research Competition
Sai Divvela University of Maryland, College Park, USA
File Attached
17:50
1h40m
Talk
E-Graph-Based Metamorphic Testing for Datalog Engines
Student Research Competition
Samuel Gerbers ETH Zurich
File Attached