| 2014 | NetKAT - A Formal System for the Verification of Networks. | Dexter Kozen |
| 2014 | Automatic Constrained Rewriting Induction towards Verifying Procedural Programs. | Cynthia Kop, Naoki Nishida |
| 2014 | Inferring Grammatical Summaries of String Values. | Se-Won Kim, Wooyoung Chin, Jimin Park, Jeongmin Kim, Sukyoung Ryu |
| 2014 | A Translation of Intersection and Union Types for the λμ-Calculus. | Kentaro Kikuchi, Takafumi Sakurai |
| 2014 | Resource Analysis of Complex Programs with Cost Equations. | Antonio Flores-Montoya, Reiner Hhnle |
| 2014 | Compositional Entailment Checking for a Fragment of Separation Logic. | Constantin Enea, Ondrej Lengl, Mihaela Sighireanu, Toms Vojnar |
| 2014 | Suppl: A Flexible Language for Policies. | Robert Dockins, Andrew Tolmach |
| 2014 | Simple and Efficient Algorithms for Octagons. | Aziem Chawdhary, Edward Robbins, Andy King |
| 2014 | A Precise and Abstract Memory Model for C Using Symbolic Values. | Frdric Besson, Sandrine Blazy, Pierre Wilke |
| 2014 | Hereditary History-Preserving Bisimilarity: Logics and Automata. | Paolo Baldan, Silvia Crafa |
| 2014 | Logic Programming and Logarithmic Space. | Clment Aubert, Marc Bagnol, Paolo Pistone, Thomas Seiller |
| 2014 | Resource Protection Using Atomics - Patterns and Verification. | Afshin Amighi, Stefan Blom, Marieke Huisman |
| 2014 | A Formalized Proof of Strong Normalization for Guarded Recursive Types. | Andreas Abel, Andrea Vezzosi |
| 2013 | Automated Inference of Library Specifications for Source-Sink Property Verification. | Haiyan Zhu, Thomas Dillig, Isil Dillig |
| 2013 | Temporal Specification Mining for Anomaly Analysis. | Farn Wang, Jung-Hsuan Wu, Chung-Hao Huang, Cheng-Chieh Chang, Chung-Cheng Li |
| 2013 | Dynamic Alias Protection with Aliasing Contracts. | Janina Voigt, Alan Mycroft |
| 2013 | Bi-Abduction with Pure Properties for Specification Inference. | Minh-Thai Trinh, Quang Loc Le, Cristina David, Wei-Ngan Chin |
| 2013 | Model Checking Dynamic Pushdown Networks. | Fu Song, Tayssir Touili |
| 2013 | The Undefined Domain: Precise Relational Information for Entities That Do Not Exist. | Holger Siegel, Bogdan Mihaila, Axel Simon |
| 2013 | Proofs, Upside Down - A Functional Correspondence between Natural Deduction and the Sequent Calculus. | Matthias Puech |
| 2013 | Semantics of Probabilistic Programs: A Weak Limit Approach. | Alessandra Di Pierro, Herbert Wiklicky |
| 2013 | Separation Logic Modulo Theories. | Juan Antonio Navarro Prez, Andrey Rybalchenko |
| 2013 | Secure Compilation of Object-Oriented Components to Protected Module Architectures. | Marco Patrignani, Dave Clarke, Frank Piessens |
| 2013 | ThisJava: An Extension of Java with Exact Types. | Hyunik Na, Sukyoung Ryu |
| 2013 | Laws of Programming for References. | Giovanny Lucero, David A. Naumann, Augusto Sampaio |