| 2026 | Auditing Rust Crates Effectively. | Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan, Caleb Stanford |
| 2026 | Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT. | Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Santacruz Del Valle, Alexandra Silva, Marco Gaboardi |
| 2026 | Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs. | Han Xu, Di Wang |
| 2026 | A Formally Verified Procedure for Width Inference in FIRRTL. | Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Fu Song, Taolue Chen, David N. Jansen |
| 2026 | Practical Refinement Session Type Inference. | Toby Ueno, Ankush Das |
| 2026 | Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism. | Hasti Toossi, Ningning Xie |
| 2026 | Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators. | Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki, Naoki Kobayashi |
| 2026 | Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing. | Philipp Schrer, Darion Haase, Joost-Pieter Katoen |
| 2026 | Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional Search. | Yasmin Sarita, Avaljot Singh, Shaurya Gomber, Gagandeep Singh, Mahesh Vishwanathan |
| 2026 | Complete Abstractions for Verification of Polymorphic Functions with Equality. | Malo Revel, Thomas Genet, Thomas P. Jensen |
| 2026 | A Formal Interface for Concurrent Search Structure Templates. | Duc-Than Nguyen, William Mansky |
| 2026 | Max-Policy Iteration, Revisited. | David Monniaux, Helmut Seidl |
| 2026 | Denotational reasoning for asynchronous multiparty session types. | Dylan McDermott, Nobuko Yoshida |
| 2026 | Lenses for Partially-Specified States. | Kazutaka Matsuda, Minh Nguyen, Meng Wang |
| 2026 | Modular Automatic Complexity Analysis of Recursive Integer Programs. | Nils Lommen, Jrgen Giesl |
| 2026 | Validating Quantum State Preparation Programs. | Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett, Alex Potanin |
| 2026 | The Memorist Tale: Every Thunk Every Cost All At Once. | Xing Li, Yao Li, Peter Schachte, Christine Rizkallah |
| 2026 | A Category-Theoretic Framework for Dependent Effect Systems. | Satoshi Kura, Marco Gaboardi, Taro Sekiyama, Hiroshi Unno |
| 2026 | Causal-Broadcast Memory. | Amir Karniel, Ori Lahav |
| 2026 | Formal Methods meet Digital Twins: Challenges and Opportunities. | Einar Broch Johnsen, Eduard Kamburjan, Andrea Pferscher, Silvia Lizeth Tapia Tarifa |
| 2026 | A Program Logic for Under-approximating Worst-case Resource Usage. | Ziyue Jin, Di Wang |
| 2026 | Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops. | Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler |
| 2026 | Specification-Driven Generation of Summaries for Symbolic Execution. | Rafael Gonalves, Frederico Ramos, Pedro Ado, Jos Fragoso Santos |
| 2026 | Reduction for Structured Concurrent Programs. | Namratha Gangamreddypalli, Constantin Enea, Shaz Qadeer |
| 2026 | Rely-Guarantee Is Coinductive - - A Proof-Centered Investigation of Inductively Approximated Coinduction -. | John Derrick, Chelsea Edmonds, Andrei Popescu, Jamie Wright |