ETAPS 2021: 27 March-1 April 2021, Luxembourg, Luxembourg (online)

ESOP 2020 programme

All times are in CEST (GMT+2)

Monday, March 29

09h00 -

10h20

ESOP

ESOP'20 Session 1 (Chair: Siddharth Krishna)

  • Andreea Costea, Amy Zhu, Nadia Polikarpova and Ilya Sergey. Concise Read-Only Specifications for Better Synthesis of Programs with Pointers [doi]
  • Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Gregersen and Lars Birkedal. Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems [doi]
  • Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens and Mark Batty. Modular Relaxed Dependencies in Weak Memory Concurrency [doi]
  • Carmine Abate, Roberto Blanco, Stefan Ciobaca, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter and Jérémy Thibault. Trace-Relating Compiler Correctness and Secure Compilation [doi] (nominated for EATCS best paper award)
15h20 - 16h40

ESOP

ESOP'20 Session 2 (Chair: Andrej Bauer)

  • Brandon Bohrer and André Platzer. Constructive Game Logic [doi]
  • Jacob Laurel and Sasa Misailovic. Continualization of Probabilistic Programs With Correction [doi]
  • Kimball Germane and Michael Adams. Compositional Control-Flow Analysis [doi]
  • Konstantinos Mamouras. Semantic Foundations for Deterministic Dataflow and Stream Processing [doi]
Tuesday, March 30

09h00 -

10h00

ESOP

ESOP'20 Session 3 (Chair: Peter Müller)

  • Sung-Shik Jongmans and Nobuko Yoshida. Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types [doi]
  • Jack Williams, Nima Joharizadeh, Andrew Gordon and Advait Sarkar. Higher-Order Spreadsheets with Spilled Arrays [doi]
  • Sreeja S. Nair, Gustavo Petri and Marc Shapiro. Proving the safety of highly-available distributed objects [doi] (nominated for EASST best paper award)
Wednesday, March 31

09h00 -

10h20

ESOP

ESOP'20 Session 4 (Chair: Nobuko Yoshida)

  • Danel Ahman and Andrej Bauer. Runners in action [doi]
  • Francesco Dagnino, Viviana Bono, Elena Zucca and Mariangiola Dezani-Ciancaglini. Soundness conditions for big-step semantics [doi]
  • Vasco Vasconcelos, Filipe Casal, Bernardo Almeida and Andreia Mordido. Mixed Sessions [doi]
  • Yusuke Matsushita, Takeshi Tsukada and Naoki Kobayashi. RustHorn: CHC-based Verification for Rust Programs [doi]
Thursday, April 1

09h00 -

10h20

ESOP

ESOP'20 Session 5 (Chair: Mark Batty)

  • 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 [doi]
  • Ákos Hajdu and Dejan Jovanović. SMT-Friendly Formalization of the Solidity Memory Model [doi]
  • Siddharth Krishna, Michael Emmi, Constantin Enea and Dejan Jovanović. Verifying Visibility-Based Weak Consistency [doi]
  • Siddharth Krishna, Alexander J. Summers, Thomas Wies. Local Reasoning for Global Graph Properties [doi]
17h00 - 18h00

FASE/ESOP

Mixed ETAPS'20 session (Chair: Konstantinos Mamouras)

  • (FASE'20) Aren Babikian, Oszkár Semeráth and Dániel Varró. Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers [doi]
  • (ESOP'20) William Mansky, Wolf Honore and Andrew Appel. Connecting Higher-Order Separation Logic to a First-Order Outside World [doi]
  • (ESOP'20) Adithya Murali, Lucas Peña, Christof Löding, P. Madhusudan. A First-Order Logic with Frames [doi] (nominated for EASST best paper award)