Talks

Below you will find slides and/or videos from talks about our work.

• Debugging and improving the C/C++11 memory model [PDF]
  Viktor Vafeiadis, overview talk, January 2016
• Software verification under weak memory consistency [PDF]
  Viktor Vafeiadis, overview talk, January 2016
• The category-theoretic solution of recursive ultra-metric space equations [PDF]
  Amin Timany, workshop talk (CoqPL'16), 23 January 2016
• Reasoning about consistency choices in distributed systems [PDF]
  Alexey Gotsman, POPL'16, 21 January 2016
• Property-Directed Abstract Interpretation [PDF]
  Noam Rinetzky, conference talk (VMCAI'16), 17 January 2016
• First Steps Towards Cumulative Inductive Types in CIC [PDF]
  Amin Timany, conference talk (ICTAC'15), 31 October 2015
• Transaction chopping for parallel snapshot isolation [PDF]
  Andrea Cerone, DISC'15, 8 October 2015
• Reasoning under release-acquire consistency [PDF]
  Viktor Vafeiadis, invited talk at GandALF'15, 22 September 2015
• Modularity in Lattices: A Case Study on the Correspondence between Top-Down and Bottom-Up Analyses [PDF]
  Noam Rinetzky, conference talk (SAS'16), 10 September 2015
• Modular Verification of Concurrency-Aware Linearizability [PDF]
  Nir Hemed, conference talk (DISC'15), 10 August 2015
• Relational Views Framework for Proving Linearizability [PDF]
  Artem Khyzha, Imperial College Concurrency Workshop, UK, July 2015
• Modular termination verification [PDF] [Video]
  Bart Jacobs, conference talk (ECOOP'15), 10 July 2015
• Provably live exception handling [PDF]
  Bart Jacobs, workshop talk (FTfJP'15), 7 July 2015
• Category Theory in Coq 8.5 [PDF]
  Amin Timany, workshop talk (Coq Workshop 2015), 26 June 2015
• Verifying read-copy-update in logic for weak memory [MP4]
  Joseph Tassarotti, 1min video abstract for PLDI 2015, June 2015
• A Formal C Memory Model Supporting Integer-Pointer Casts [MP4]
  Jeehoon Kang, 1min video abstract for PLDI 2015, 16 June 2015
• Software verification under weak memory consistency [PDF]
  Viktor Vafeiadis, invited talk at Dagstuhl seminar, 4 May 2015
• Composite replicated data types [PDF]
  Alexey Gotsman, ESOP'15, 16 April 2015
• Sound, modular and compositional verification of the input/output behavior of programs [PDF]
  Willem Penninckx, ESOP'15, 14 April 2015
• Proving Lock-Freedom Easily and Automatically [PDF]
  Viktor Vafeiadis, CPP 2015, 14 January 2015
• Program logics for relaxed consistency [PDF (Part I)] [PDF (Part II)]
  Viktor Vafeiadis, UPMARC Summer School, 28-29 July 2014
  
• Reasoning about the C/C++ weak memory model [PDF]
  Viktor Vafeiadis, invited talk at (EC)2, 17 July 2014
  
• A case for relaxed program logics [PDF]
  Viktor Vafeiadis, IHP trimester on proofs, 17 July 2014
  
• Brief Announcement: Concurrency-Aware Linearizability [PDF]
  Nir Hemed, conference talk (PODC'14), 17 July 2014
• Parameterised Linearisability [PDF]
  Andrea Cerone, ICALP 2014, 8 July 2014
  
• Reasoning about eventual consistency and replicated data types [PDF]
  Alexey Gotsman, MSR-IMDEA Collaboration Workshop, 4 April 2014
• Relaxed Separation Logic [PDF]
  Viktor Vafeiadis, POPL 2014 Tutorials, 20 January 2014
• Verifying Concurrent Memory Reclamation Algorithms with Grace + From Hoare Logic to Separation Logic [PDF]
  Noam Rinetzky, Technion, 1 July 2013
  
• Verifying TSO Programs [PDF]
  Bart Jacobs, MSRC Workshop on Verified Concurrent Programs, 12 June 2013