SMT solver bugs, including soundness issues, crashes, and assertion failures, can silently corrupt verification results. We present CAST, to our knowledge the first continuous fuzzing service for SMT solvers, integrating differential testing and type-aware mutation into CI pipelines with commit-aware corpus reduction. In a 90-day evaluation on CVC5 and Z3, CAST found 42 bugs (12 soundness issues), 33 confirmed and fixed upstream, none dismissed as invalid, with 99.2% workflow success rate over 14,006 workflow executions. Corpus reduction achieves 37.0% (CVC5) and 80.6% (Z3) average reduction while maintaining coverage of changed code. Continued operation has found 46 bugs to date.

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