ESOP 2018 Accepted Papers

  • Lars Hupel, Tobias Nipkow (Technische Universität München). A Verified Compiler from Isabelle/HOL to CakeML
  • Lau Skorstengaard (Aarhus University); Dominique Devriese (imec-DistriNet, KU Leuven); Lars Birkedal (Aarhus University). Reasoning About a Capability Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management (without OS Support)
  • Marco Eilers, Peter Müller, Samuel Hitz (ETH Zurich). Modular Product Programs
  • Xuan Bach Le, Aquinas Hobor (National University of Singapore). Logical Reasoning over Disjoint Permissions
  • Krishnendu Chatterjee, Amir Kafshdar Goharshady (IST Austria); Yaron Velner (Hebrew University of Jerusalem). Quantitative Analysis of Smart Contracts
  • Bernardo Toninho, Nobuko Yoshida (Imperial College London). On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings
  • Tobias Kappé, Paul Brunet, Alexandra Silva, Fabio Zanasi (University College London). Concurrent Kleene Algebra: Free Model and Completeness
  • Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe (The University of Tokyo). Higher-Order Program Verification via HFL Model Checking
  • Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja (RWTH Aachen University). How long, O Bayesian network, will I sample thee?
  • Brandon Moore (Runtime Verification, Inc.); Lucas Peña, Grigore Rosu (University of Illinois at Urbana-Champaign). Program Verification by Coinduction
  • Shiyi Wei (The University of Texas at Dallas); Piotr Mardziel (Carnegie Mellon University); Andrew Ruef, Jeffrey S. Foster, Michael Hicks (University of Maryland, College Park). Evaluating Design Tradeoffs in Numeric Static Analysis for Java
  • Pierre-Marie Pédrot (Max Planck Institute); nicolas tabareau (Inria Nantes, France). Failure is Not an Option: An Exceptional Type Theory
  • Alex Simpson, Niels Voorneveld (University of Ljubljana). Behavioural equivalence via modalities for algebraic effects
  • Caterina Urban, Peter Müller (ETH Zurich, Switzerland). An Abstract Interpretation Framework for Input Data Usage
  • Jafar Hamin, Bart Jacobs (imec-distrinet, Dept. C.S., KU Leuven). Deadlock-Free Condition Variables
  • Klaus Ostermann, Julian Jabs (University of Tuebingen, Germany). Dualizing Generalized Algebraic Data Types by Matrix Transposition
  • Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira (The University of Hong Kong). Consistent Subtyping for All
  • Amr Hany Saleh, Georgios Karachalias (KU Leuven); Matija Pretnar (University of Ljubljana); Tom Schrijvers (KU Leuven). Explicit Effect Subtyping
  • Alejandro Aguirre, Gilles Barthe (IMDEA Software Institute); Lars Birkedal, Aleš Bizjak (Aarhus University); Marco Gaboardi (University at Buffalo, SUNY); Deepak Garg (MPI-SWS). Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
  • Kasper Svendsen, Jean Pichon-Pharabod (University of Cambridge); Marko Doko (MPI-SWS); Ori Lahav (Tel Aviv University); Viktor Vafeiadis (MPI-SWS). A separation logic for a promising semantics
  • Azalea Raad (MPI-SWS, Germany); Ori Lahav (Tel Aviv University, Israel); Viktor Vafeiadis (MPI-SWS, Germany). On Parallel Snapshot Isolation and Release/Acquire Consistency
  • Mike Dodds (Galois Inc.); Mark Batty (University of Kent); Alexey Gotsman (IMDEA Software Institute). Compositional Verification of Compiler Optimisations on Relaxed Memory
  • Juliana Vicente Franco (Imperial College London); Sylvan Clebsch (Microsoft Research, Cambridge); Sophia Drossopoulou (Imperial College London); Jan Vitek (Northeastern University, Boston & CVUT, Prague); Tobias Wrigstad (Uppsala University, Uppsala). Correctness of a fully concurrent Garbage Collector for Actor Languages
  • Vincent Rahli, Ivana Vukotic, Marcus Volp, Paulo Verissimo (SnT, University of Luxembourg). Belisarius: Byzantine Fault Tolerant Protocols Powered by Coq
  • Malte Viering, Tzu-Chun Chen (TU Darmstadt, Germany); Patrick Eugster (TU Darmstadt, Germany; Università della Svizzera italiana, Switzerland; Purdue University, USA); Raymond Hu (Imperial College London, UK); Lukasz Ziarek (SUNY Buffalo, USA). A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems
  • Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman (IMDEA Software Institute); Ilya Sergey (University College London). Paxos Consensus, Deconstructed and Abstracted
  • Gilles Barthe (IMDEA Software Institute); Thomas Espitau (Université Pierre et Marie Curie); Marco Gaboardi (University at Buffalo, SUNY); Benjamin Grégoire (Inria); Justin Hsu (University College London); Pierre-Yves Strub (École Polytechnique). A Program Logic for Probabilistic Programs
  • Radha Jagadeesan, James Riely. Eventual Consistency for CRDTs
  • Hannah Gommerstadt, Limin Jia, Frank Pfenning (Carnegie Mellon University). Session-Typed Concurrent Contracts
  • Samuel Merten, Alexander Bagnall, Gordon Stewart (Ohio University). Verified Learning Without Regret
  • Parosh Aziz Abdulla, Bengt Jonsson, Cong Quy Trinh (Uppsala University). Fragment Abstraction for Concurrent Shape Analysis
  • Ningning Xie, Bruno C. d. S. Oliveira (The University of Hong Kong). Let Arguments Go First
  • Benjamin Bichsel, Timon Gehr, Martin Vechev (ETH Zürich). Fine-grained Semantics for Probabilistic Programs
  • Armaël Guéneau (Inria Paris); Arthur Charguéraud (Inria); François Pottier (Inria Paris). A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification
  • Joaquin Aguado, Michael Mendler (University of Bamberg); Marc Pouzet (École Normale Supérieure (ENS)); Partha Roop (University of Auckland); Reinhard von Hanxleden (University of Kiel). Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach
  • Kazutaka Matsuda (Tohoku University); Meng Wang (University of Kent). HOBiT: Programming Lenses without using Lens Combinators