| 2014 | Verified Compilation for Shared-Memory C. | Lennart Beringer, Gordon Stewart, Robert Dockins, Andrew W. Appel |
| 2014 | A Coq Formalization of the Relational Data Model. | Vronique Benzaken, Evelyne Contejean, Stefania Dumbrava |
| 2014 | Grounding Synchronous Deterministic Concurrency in Sequential Programming. | Joaqun Aguado, Michael Mendler, Reinhard von Hanxleden, Insa Fuhrmann |
| 2013 | Ribbon Proofs for Separation Logic. | John Wickerson, Mike Dodds, Matthew J. Parkinson |
| 2013 | Abstract Refinement Types. | Niki Vazou, Patrick Maxim Rondon, Ranjit Jhala |
| 2013 | Higher-Order Processes, Functions, and Sessions: A Monadic Integration. | Bernardo Toninho, Lus Caires, Frank Pfenning |
| 2013 | Constraining Delimited Control with Contracts. | Asumu Takikawa, T. Stephen Strickland, Sam Tobin-Hochstadt |
| 2013 | Modular Reasoning about Separation of Concurrent Data Structures. | Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson |
| 2013 | Counterexample-Guided Precondition Inference. | Mohamed Nassim Seghir, Daniel Kroening |
| 2013 | GADTs Meet Subtyping. | Gabriel Scherer, Didier Rmy |
| 2013 | On Distributability in Process Calculi. | Kirstin Peters, Uwe Nestmann, Ursula Goltz |
| 2013 | Distributed Electronic Rights in JavaScript. | Mark S. Miller, Tom Van Cutsem, Bill Tulloh |
| 2013 | FliPpr: A Prettier Invertible Printing System. | Kazutaka Matsuda, Meng Wang |
| 2013 | Concurrent Flexible Reversibility. | Ivan Lanese, Michael Lienhardt, Claudio Antares Mezzina, Alan Schmitt, Jean-Bernard Stefani |
| 2013 | Model-Checking Higher-Order Programs with Recursive Types. | Naoki Kobayashi, Atsushi Igarashi |
| 2013 | Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems. | Joost-Pieter Katoen, Doron A. Peled |
| 2013 | A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness. | Ioannis T. Kassios, Eleftherios Kritikos |
| 2013 | Language Constructs for Non-Well-Founded Computation. | Jean-Baptiste Jeannin, Dexter Kozen, Alexandra Silva |
| 2013 | Quarantining Weakness - Compositional Reasoning under Relaxed Memory Models (Extended Abstract). | Radha Jagadeesan, Gustavo Petri, Corin Pitcher, James Riely |
| 2013 | Automatic Type Inference for Amortised Heap-Space Analysis. | Martin Hofmann, Dulma Rodriguez |
| 2013 | Verifying Concurrent Memory Reclamation Algorithms with Grace. | Alexey Gotsman, Noam Rinetzky, Hongseok Yang |
| 2013 | Why3 - Where Programs Meet Provers. | Jean-Christophe Fillitre, Andrei Paskevich |
| 2013 | Compositional Invariant Checking for Overlaid and Nested Linked Lists. | Constantin Enea, Vlad Saveluc, Mihaela Sighireanu |
| 2013 | Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels. | Peter Collingbourne, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer |
| 2013 | Pretty-Big-Step Semantics. | Arthur Charguraud |