ESOP 2020 programme

09h00 -

10h20

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)

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]

09h00 -

10h00

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)

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]

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]

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)