kirancodes.me
To Proof Maintenance & Beyond!
Venues / ESOP /

ESOP 2020

27 papers

  1. A First-Order Logic with Frames · Adithya Murali, Lucas Peña, Christof Löding, P. Madhusudan
  2. ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures · Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget + 1 more
  3. Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems · Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal
  4. ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs · John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi
  5. Concise Read-Only Specifications for Better Synthesis of Programs with Pointers · Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey
  6. Connecting Higher-Order Separation Logic to a First-Order Outside World · William Mansky, Wolf Honoré, Andrew W. Appel
  7. Constructive Game Logic · Rose Bohrer, André Platzer
  8. Continualization of Probabilistic Programs With Correction · Jacob Laurel, Sasa Misailovic
  9. Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types · Sung-Shik Jongmans, Nobuko Yoshida
  10. Higher-Order Spreadsheets with Spilled Arrays · Jack Williams, Nima Joharizadeh, Andrew D. Gordon, Advait Sarkar
  11. Higher-Ranked Annotation Polymorphic Dependency Analysis · Fabian Thorand, Jurriaan Hage
  12. Liberate Abstract Garbage Collection from the Stack by Decomposing the Heap · Kimball Germane, Michael D. Adams
  13. Local Reasoning for Global Graph Properties · Siddharth Krishna, Alexander J. Summers, Thomas Wies
  14. Mixed Sessions · Vasco T. Vasconcelos, Filipe Casal, Bernardo Almeida, Andreia Mordido
  15. Modular Inference of Linear Types for Multiplicity-Annotated Arrows · Kazutaka Matsuda
  16. Modular Relaxed Dependencies in Weak Memory Concurrency · Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, Mark Batty
  17. On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem · Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
  18. Optimal and Perfectly Parallel Algorithms for On-demand Data-Flow Analysis · Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis
  19. Proving the Safety of Highly-Available Distributed Objects · Sreeja S. Nair, Gustavo Petri, Marc Shapiro
  20. Runners in Action · Danel Ahman, Andrej Bauer
  21. RustHorn: CHC-Based Verification for Rust Programs · Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
  22. SMT-Friendly Formalization of the Solidity Memory Model · Ákos Hajdu, Dejan Jovanovic
  23. Semantic Foundations for Deterministic Dataflow and Stream Processing · Konstantinos Mamouras
  24. Solving Program Sketches with Large Integer Values · Rong Pan, Qinheping Hu, Rishabh Singh, Loris D'Antoni
  25. Soundness Conditions for Big-Step Semantics · Francesco Dagnino, Viviana Bono, Elena Zucca, Mariangiola Dezani-Ciancaglini
  26. Trace-Relating Compiler Correctness and Secure Compilation · Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu + 3 more
  27. Verifying Visibility-Based Weak Consistency · Siddharth Krishna, Michael Emmi, Constantin Enea, Dejan Jovanovic