The thirty-nine papers.

• Continuity Analysis of Programs. By Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman.
  
• Compositional May-Must Program Analysis: Unleashing the Power of Alternation. By Patrice Godefroid, Aditya Nori, Sriram Rajamani, Sai Tetali.
  
• Nominal System T. By Andrew Pitts.
  
• Structuring the verification of heap-manipulating programs. By Aleks Nanevski, Viktor Vefeiadis, Josh Berdine.
  
• Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification. By Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno.
  
• Type Inference for Datalog with Complex Type Hierarchies. By Max Schaefer, Oege de Moor.
  
• Coarse-Grained Transactions. By Eric Koskinen, Matthew Parkinson, Maurice Herlihy.
  
• A Theory of Indirection via Approximation. By Aquinas Hobor, Robert Dockins, Andrew Appel.
  
• Semantics and Algorithms for Data-dependent Grammars. By Yitzhak Mandelbaum, Trevor Jim, David Walker.
  
• Verified just-in-time compiler on x86. By Magnus Myreen.
  
• Automatically Generating Back Ends Using Declarative Machine Descriptions. By Joao Dias, Norman Ramsey.
  
• Pure Subtype Systems. By DeLesley Hutchins.
  
• A simple, verified validator for software pipelining. By Jean-Baptiste Tristan, Xavier Leroy.
  
• Integrating Typed and Untyped Code in a Scripting Language. By Tobias Wrigstad, F. Zappa Nardelli, Sylvain Lebresne, Johan Ostlund, Jan Vitek.
  
• Contracts Made Manifest. By Michael Greenberg, Benjamin Pierce, Stephanie Weirich.
  
• Automatic Numeric Abstractions for Heap-Manipulating Programs. By Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay.
  
• Low-Level Liquid Types. By Patrick Rondon, Ranjit Jhala, Ming Kawaguchi.
  
• Modular Session Types for Distributed Object-Oriented Programming. By Simon Gay, Vasco Vasconcelos, Antonio Ravara, Nils Gesbert, Alexandre Caldeira.
  
• Nested Interpolants. By Mattias Heizmann, Jochen Hoenicke, Andreas Podelski.
  
• Dynamically Checking Ownership Policies in Concurrent C/C++ Programs. By Jean-Phillipe Martin, Michael Hicks, Manuel Costa, Periklis Akritidis, Miguel Castro.
  
• Program Analysis via Satisfiability Modulo Path Programs. By William Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta.
  
• Sequential Verification of Serializability. By Hagit Attiya, G. Ramalingam, Noam Rinetzky.
  
• Toward a Verified Relational Database Management System. By Ryan Wisnesky, Gregory Malecha, Avraham Shinnar, Greg Morrisett.
  
• Static Determination of Quantitative Resource Usage for Higher-Order Programs. By Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Martin Hofmann.
  
• Dependent types and program equivalence. By Limin Jia, Jianzhou Zhao, Vilhelm Sjoberg, Stephanie Weirich.
  
• A Relational Modal Logic for Higher-Order Stateful ADTs. By Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal.
  
• A Verified Compiler for an Impure Functional Language. By Adam Chlipala.
  
• Threesomes, With and Without Blame. By Jeremy Siek, Philip Wadler.
  
• On the Verification Problem for Weak Memory Models. By Mohamed Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madan Musuvathi.
  
• Generating Compiler Optimizations from Proofs. By Ross Tate, Michael Stepp, Sorin Lerner.
  
• Counterexample-Guided Focus. By Andreas Podelski, Thomas Wies.
  
• Modular Verification of Security Protocol Code by Typing. By Karthikeyan Bhargavan, Cedric Fournet, Andrew Gordon.
  
• From Program Verification to Program Synthesis. By Saurabh Srivastava, Sumit Gulwani, Jeffrey Foster.
  
• Dependent Types from Counterexamples. By Tachio Terauchi.
  
• Abstraction-Guided Synthesis. By Martin Vechev, Eran Yahav, Greta Yorsh.
  
• Programming with Angelic Non-determinism. By Joel Galenson, Casey Rodarmor, Nicholas Tung, Satish Chandra, Rastislav Bodik.
  
• Monads in Action. By Andrzej Filinski.
  
• Paralocks - Role-Based Information Flow Control and Beyond. By Niklas Broberg, David Sands.
  
• Decision Procedures for Algebraic Data Types with Abstractions. By Philippe Suter, Mirco Dotta, Viktor Kuncak.