| 2015 | A Scalable, Correct Time-Stamped Stack. | Mike Dodds, Andreas Haas, Christoph M. Kirsch |
| 2015 | Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. | Benjamin Delaware, Clment Pit-Claudel, Jason Gross, Adam Chlipala |
| 2015 | A Calculus for Relaxed Memory. | Karl Crary, Michael J. Sullivan |
| 2015 | Program Boosting: Program Synthesis via Crowd-Sourcing. | Robert A. Cochran, Loris D'Antoni, Benjamin Livshits, David Molnar, Margus Veanes |
| 2015 | Proof engineering: implementation challenges in rigorously verified software. | Adam Chlipala |
| 2015 | From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. | Adam Chlipala |
| 2015 | Ur/Web: A Simple Model for Programming the Web. | Adam Chlipala |
| 2015 | Quantitative Interprocedural Analysis. | Krishnendu Chatterjee, Andreas Pavlogiannis, Yaron Velner |
| 2015 | Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth. | Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, Prateesh Goyal |
| 2015 | Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction. | Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Pietro Abate |
| 2015 | Databases and Programming: Two Subjects Divided by a Common Language? | Peter Buneman |
| 2015 | Self-Representation in Girard's System U. | Matt Brown, Jens Palsberg |
| 2015 | Tractable Refinement Checking for Concurrent Objects. | Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza |
| 2015 | Full Abstraction for Signal Flow Graphs. | Filippo Bonchi, Pawel Sobocinski, Fabio Zanasi |
| 2015 | K-Java: A Complete Semantics of Java. | Denis Bogdanas, Grigore Rosu |
| 2015 | Formal verification of compilers and static analyzers. | Sandrine Blazy |
| 2015 | Specification Inference Using Context-Free Language Reachability. | Osbert Bastani, Saswat Anand, Alex Aiken |
| 2015 | Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. | Gilles Barthe, Marco Gaboardi, Emilio Jess Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub |
| 2015 | DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations. | Rajeev Alur, Loris D'Antoni, Mukund Raghothaman |
| 2015 | Sound Modular Verification of C Code Executing in an Unverified Context. | Pieter Agten, Bart Jacobs, Frank Piessens |
| 2015 | Towards the Essence of Hygiene. | Michael D. Adams |
| 2014 | Toward general diagnosis of static errors. | Danfeng Zhang, Andrew C. Myers |
| 2014 | TDVMP: Improved Virtual Machine-Based Software Protection with Time Diversity. | Huaijun Wang, Dingyi Fang, Guanghui Li, Na An, Xiaojiang Chen, Yuanxiang Gu |
| 2014 | Gradual typing embedded securely in JavaScript. | Nikhil Swamy, Cdric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman |
| 2014 | The GDSL toolkit: Generating Frontends for the Analysis of Machine Code. | Axel Simon, Julian Kranz |