| 2013 | Quantitative abstraction refinement. | Pavol Cern, Thomas A. Henzinger, Arjun Radhakrishna |
| 2013 | Deadlock-freedom-by-design: multiparty asynchronous global programming. | Marco Carbone, Fabrizio Montesi |
| 2013 | The type discipline of behavioral separation. | Lus Caires, Joo Costa Seco |
| 2013 | BinSlayer: accurate comparison of binary executables. | Martial Bourquin, Andy King, Edward Robbins |
| 2013 | Sigma*: symbolic learning of input-output specifications. | Matko Botincan, Domagoj Babic |
| 2013 | Checking NFA equivalence with bisimulations up to congruence. | Filippo Bonchi, Damien Pous |
| 2013 | Cache and I/O efficent functional algorithms. | Guy E. Blelloch, Robert Harper |
| 2013 | Static and dynamic semantics of NoSQL languages. | Vronique Benzaken, Giuseppe Castagna, Kim Nguyen, Jrme Simon |
| 2013 | On the linear ranking problem for integer linear-constraint loops. | Amir M. Ben-Amram, Samir Genaim |
| 2013 | Library abstraction for C/C++ concurrency. | Mark Batty, Mike Dodds, Alexey Gotsman |
| 2013 | Automatic detection of floating-point exceptions. | Earl T. Barr, Thanh Vo, Vu Le, Zhendong Su |
| 2013 | Abstraction and invariance for algebraically indexed types. | Robert Atkey, Patricia Johann, Andrew Kennedy |
| 2013 | Principled parsing for indentation-sensitive languages: revisiting landin's offside rule. | Michael D. Adams |
| 2013 | Streaming big data with self-adjusting computation. | Umut A. Acar, Yan Chen |
| 2013 | Copatterns: programming infinite structures by observations. | Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer |
| 2012 | Randomized accuracy-aware program transformations for efficient approximate computations. | Zeyuan Allen Zhu, Sasa Misailovic, Jonathan A. Kelner, Martin C. Rinard |
| 2012 | Formalizing the LLVM intermediate representation for verified program transformations. | Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic |
| 2012 | A language for automatically enforcing privacy policies. | Jean Yang, Kuat Yessenov, Armando Solar-Lezama |
| 2012 | Or-parallel prolog execution on multicores based on stack splitting. | Rui Vieira, Ricardo Rocha, Fernando M. A. Silva |
| 2012 | Symbolic finite state transducers: algorithms and applications. | Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, Nikolaj S. Bjrner |
| 2012 | Self-certification: bootstrapping certified typecheckers in F* with Coq. | Pierre-Yves Strub, Nikhil Swamy, Cdric Fournet, Juan Chen |
| 2012 | Static and user-extensible proof checking. | Antonis Stampoulis, Zhong Shao |
| 2012 | Freefinement. | Stephan van Staden, Cristiano Calcagno, Bertrand Meyer |
| 2012 | Sound predictive race detection in polynomial time. | Yannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, Cormac Flanagan |
| 2012 | Multi-DaC programming model: a variant of multi-BSP model for divide-and-conquer algorithms. | Abdorreza Savadi, Morteza Moradi, Hossein Deldari |