ESOP 2020 Accepted Papers

  • Andreea Costea, Amy Zhu, Nadia Polikarpova and Ilya Sergey. Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
  • Fabian Thorand and Jurriaan Hage. Higher-Ranked Annotation Polymorphic Dependency Analysis
  • Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen and Andreas Pavlogiannis. Optimal and Perfectly Parallel Algorithms for On-demand Data-flow Analysis
  • Rong Pan, Qinheping Hu, Rishabh Singh and Loris D'Antoni. Solving Program Sketches with Large Integer Values
  • Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Gregersen and Lars Birkedal. Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
  • Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens and Mark Batty. Modular Relaxed Dependencies in Weak Memory Concurrency
  • Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter and Jérémy Thibault. Trace-Relating Compiler Correctness and Secure Compilation
  • Sung-Shik Jongmans and Nobuko Yoshida. Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types
  • Siddharth Krishna, Michael Emmi, Constantin Enea and Dejan Jovanovic. Verifying Visibility-Based Weak Consistency
  • John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi and Naoki Kobayashi. ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
  • Kazutaka Matsuda. A Modular Inference of Linear Types for Multiplicity-Annotated Arrows
  • Sreeja S Nair, Gustavo Petri and Marc Shapiro. Proving the safety of highly-available distributed objects
  • William Mansky, Wolf Honore and Andrew Appel. Connecting Higher-Order Separation Logic to a First-Order Outside World
  • Danel Ahman and Andrej Bauer. Runners in action
  • Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget and Peter Sewell. ARMv8-A system semantics: instruction fetch in relaxed architectures
  • Francesco Dagnino, Viviana Bono, Elena Zucca and Mariangiola Dezani-Ciancaglini. Soundness conditions for big-step semantics
  • Christof Löding, P. Madhusudan, Adithya Murali and Lucas Peña. A First-Order Logic with Frames
  • Brandon Bohrer and André Platzer. Constructive Game Logic
  • Jacob Laurel and Sasa Misailovic. Continualization of Probabilistic Programs With Correction
  • Kimball Germane and Michael Adams. Compositional Control-Flow Analysis
  • Vasco Vasconcelos, Filipe Casal, Bernardo Almeida and Andreia Mordido. Mixed Sessions
  • Yusuke Matsushita, Takeshi Tsukada and Naoki Kobayashi. RustHorn: CHC-based Verification for Rust Programs
  • Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago and Francesco Gavazzo. On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
  • Ákos Hajdu and Dejan Jovanović. SMT-Friendly Formalization of the Solidity Memory Model
  • Jack Williams, Nima Joharizadeh, Andrew Gordon and Advait Sarkar. Higher-Order Spreadsheets with Spilled Arrays
  • Siddharth Krishna, Alexander J. Summers and Thomas Wies. >Local Reasoning for Global Graph Properties
  • Konstantinos Mamouras. Semantic Foundations for Deterministic Dataflow and Stream Processing