Programs that integrate LLM APIs routinely send sensitive data to external services and execute LLM-generated strings as database queries, shell commands, or API calls. No existing type system or static analysis captures the security properties of these interactions. We present LLMEffect, a type-and-effect system for LLM-integrated programs. LLMEffect assigns security labels to data flowing into LLM calls, enforces a typestate discipline on LLM output before it can reach dangerous operations, and provides a dual-bound iteration model that distinguishes productive agent steps from error-recovery loops. We describe the design of LLMEffect and outline a Python-based implementation with an accompanying static analyzer.

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