| 2017 | Weakly Sensitive Analysis for Unbounded Iteration over JavaScript Objects. | Yoonseok Ko, Xavier Rival, Sukyoung Ryu |
| 2017 | Sound and Efficient Language-Integrated Query - Maintaining the ORDER. | Oleg Kiselyov, Tatsuya Katsushima |
| 2017 | Decision Procedure for Entailment of Symbolic Heaps with Arrays. | Daisuke Kimura, Makoto Tatsuta |
| 2017 | Safety and Liveness of MCS Lock - Layer by Layer. | Jieung Kim, Vilhelm Sjberg, Ronghui Gu, Zhong Shao |
| 2017 | Counterexample-Guided Bit-Precision Selection. | Shaobo He, Zvonimir Rakamaric |
| 2017 | Capabilities for Java: Secure Access to Resources. | Ian J. Hayes, Xi Wu, Larissa A. Meinicke |
| 2017 | Programming by Examples: PL Meets ML. | Sumit Gulwani, Prateek Jain |
| 2017 | Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications. | Neline van Ginkel, Raoul Strackx, Frank Piessens |
| 2017 | Enforcing Programming Guidelines with Region Types and Effects. | Serdar Erbatur, Martin Hofmann, Eugen Zalinescu |
| 2017 | A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls. | Alejandro Daz-Caro |
| 2017 | Black-Box Equivalence Checking Across Compiler Optimizations. | Manjeet Dahiya, Sorav Bansal |
| 2017 | Compact Difference Bound Matrices. | Aziem Chawdhary, Andy King |
| 2017 | Bringing Order to the Separation Logic Jungle. | Qinxiang Cao, Santiago Cullar, Andrew W. Appel |
| 2017 | The Negligible and Yet Subtle Cost of Pattern Matching. | Beniamino Accattoli, Bruno Barras |
| 2016 | Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation. | Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi |
| 2016 | Unified Syntax with Iso-types. | Yanpeng Yang, Xuan Bi, Bruno C. d. S. Oliveira |
| 2016 | A Sound and Complete Bisimulation for Contextual Equivalence in \lambda -Calculus with Call/cc. | Taichi Yachi, Eijiro Sumii |
| 2016 | SPEC: An Equivalence Checker for Security Protocols. | Alwen Tiu, Nam Nguyen, Ross Horne |
| 2016 | Higher-Order Model Checking in Direct Style. | Taku Terao, Takeshi Tsukada, Naoki Kobayashi |
| 2016 | Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic. | Makoto Tatsuta, Quang Loc Le, Wei-Ngan Chin |
| 2016 | AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code. | Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi, Priya Narasimhan |
| 2016 | Static Trace-Based Deadlock Analysis for Synchronous Mini-Go. | Kai Stadtmller, Martin Sulzmann, Peter Thiemann |
| 2016 | AkkaProf: A Profiler for Akka Actors in Parallel and Distributed Applications. | Andrea Ros, Lydia Y. Chen, Walter Binder |
| 2016 | Eliom: A Core ML Language for Tierless Web Programming. | Gabriel Radanne, Jrme Vouillon, Vincent Balat |
| 2016 | DOM: Specification and Client Reasoning. | Azalea Raad, Jos Fragoso Santos, Philippa Gardner |