CSL Family Tree

With the recently increased interest in the CS community to concurrency verification, this slide, which I’ve made sometime ago and which depicts the “flow of ideas” between modern concurrency logics, became very popular, so I decided to put it online for anyone who might want to use it in a presentation. I will keep it updated with more logics to come. Feel free to drop me a line if you need the diagram’s sources or want me to add your favourite logic, which is missing.

Update: The CSL Family Tree depiction is now featured in the Wikipedia article on Interference freedom (courtesy of David Gries).

Talks

Invited and informal talks, workshop presentations, lectures and seminars, with the slides, are listed below. Slides for conference talks are available in the publications page.

• Compositional Verification of Composite Byzantine Protocols [Slides]
  
  • Aarhus University, Denmark, December 2024
  • IOHK Seminar, Online, December 2024
  • ETH Zürich, Switzerland, November 2024
• Proving as Programming [Slides]
  
  • Workshop on Formal Proofs and Lean, NUS, Singapore, April 2024
• Deductive Synthesis of Programs with Pointers: Expressive, Trustworthy, Fast [Slides]
  
  • University of Utah, UT, US, October 2024
  • CISPA Helmholtz Center for Information Security, Germany, March 2023
  • Seventh Conference on Software Engineering and Information Management, April 2022
  • The 4th Working Formal Methods Symposium, Babes-Bolyai University, Romania, September 2020
• CoSplit: Practical Smart Contract Sharding with Static Program Analysis [Slides]
  
  • Workshop on Dependable and Secure Software Systems, ETH Zürich, Switzerland, October 2022
  • HotSpot'21: 7th Workshop on Hot Issues in Security Principles and Trust, September 2021
  • Chalmers University, Sweden, March 2021
  • Purdue University, USA, September 2020
• Cardinality Analysis for Haskell Programs [Slides]
  
  • Chalmers University, Sweden, March 2021
• The Scilla Journey: 
 From Proof General to Thousands of Nodes [Slides]
  
  • 1st Workshop on Formal Methods for Blockchains, Porto, Portugal, October 2019
• ICFP Programming Contest 2019 Report [Slides]
  
  • ICFP 2019, Berlin, Germany, August 2019
• Functional Programming is Everywhere [Slides (PLMW@ICFP19)]
  
  • Programming Languages Mentoring Workshop @ ICFP 2019, Berlin, Germany, August 2019
• Engineering Distributed Systems that We Can Trust (and also Run) [Slides]
  
  • PODC 2019, Keynote talk, Toronto, Canada, August 2019
• Composing Software Systems that are Provably Correct [Slides]
  
  • ECOOP 2019, Dahl-Nygaard prize keynote talk, London, UK, July 2019
• Compositional Static Race Detection at Scale, without False Positives [Slides]
  
  • JetBrains, St. Petersburg, Russia, July 2019
  • National University of Singapore, April 2019
• How to Bootstrap a Research Project [Slides (PLMW@POPL19)]
  
  • Programming Languages Mentoring Workshop @ POPL 2019, Lisbon, Portugal, January 2019
• What We Talk about When We Talk about Formally Verified Systems [Slides]
  
  • Blockchain and Cybersecurity Workshop 2018, National University of Singapore, November 2018
• Safe Smart Contract Programming with Scilla [Slides]
  
  • Programming Workshop by Zilliqa, National University of Singapore, November 2018
• Deductive Synthesis of Programs that Alter Data Structures [Slides]
  
  • Aarhus University, Denmark, December 2018
  • National University of Singapore, November 2018
  • Imperial College London, UK, October 2018
  • KU Leuven, Belgium, September 2018
  • Inria Paris, France, September 2018
  • KAIST, Daejeon, Korea, August 2018
• Distributed Consensus Protocols and Their Applications [Lecture 1 | Lecture 2 | Lecture 3]
  • SIGPL 2018 Summer School, Seoul, August 2018
• Scilla: Foundations for Verifiable Decentralised Computations on a Blockchain [Slides]
  
  • The Blockchain Connector, London Blockchain Developer Meetup, London, UK, May 2018
  • PLEMM 2018: Programming Language Enthusiasts Mind Melt, Bellevue, WA, US, May 2018
  • University of California San Diego, CA, US, May 2018
• Mechanising Blockchain Consensus [Slides]
  
  • University of Utah, UT, US, May 2018
• Programming and Proving with Distributed Protocols [Slides]
  
  • University Paris Diderot – Paris 7, France, April 2018
  • Microsoft Research, Cambridge, UK, November 2017
  • National University of Singapore, October 2017
  • Heriot-Watt University, UK, July 2017
  • IMDEA Software Institute, Spain, June 2017
  • Aarhus University, Denmark, May 2017
  • University of California San Diego, USA, May 2017
  • Imperial College London, UK, November 2016
• Guarding a Gallery with Sleepy Robots [Slides]
  
  • University of California San Diego, USA, February 2019
  • Yale-NUS College, Singapore, October 2017
• Dependent Types for Verification of Real-World Programs [Slides]
  
  • Russian National Conference on Programming Languages and Compilers, Rostov-on-Don, Russia, April 2017.
• Programming and Proving with Concurrent Resources [Slides]
  
  • University of York, UK, October 2016
  • University of Cambridge, UK, June 2016
  • Aarhus University, Denmark, June 2016
  • Max Planck Institute for Software Systems, Germany, May 2016
  • Imperial College London, UK, May 2016
  • Middlesex University, UK, May 2016
  • University of Birmingham, UK, January 2016
  • Queen Mary University of London, UK, December 2015
  • University College London, UK, April 2015
  • Microsoft Research, Cambridge, UK, March 2015
• Reasoning about non-linearizable concurrent objects
  
  • Dagstuhl Seminar 16201, Germany, May 2016
  • University of Kent, UK, April 2016
• Anatomy of mechanized reasoning about fine-grained concurrency
  Dagstuhl Seminar 15191 on Compositional Verification Methods for Next-Generation Concurrency, Schloss Dagstuhl, Germany, May 2015 [Slides]
• Programming with Proofs
  Google, London, UK. April 2015.
• Towards Structured Mechanized Verification of Fine-Grained Concurrent Programs
  The First International Workshop on Coq for PL at POPL 2015. Mumbai, India. January 2015.
• Formal Mathematics as a Branch of Computer Science
  Sociological Institute of the Russian Academy of Sciences, Saint Petersburg, Russia. August 2014.
• Communicating State Transition Systems for Fine-Grained Concurrent Resources
  
  • 1st Microsoft Research and IMDEA Software Institute Collaboration Workshop (MICW 2014). Madrid, Spain. April 2014. [Slides]
  • 2nd ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE 2013). Boston, MA, USA. September 2013. [Slides]
• State Transition System alternative to Linearizability [Slides]
  Concurrency Yak at POPL 2014. San Diego, CA, USA. January 2014.
  
• Monadic Abstract Interpreters
  Invited talk at 15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013). Madird, Spain. September 2013.
  
• Static Analysis and Code Optimizations in Glasgow Haskell Compiler [Slides | SlideShare | Video]
  SPb Functional Programming meetup. Saint Petersburg, Russia. December 2012.
  
• Dominance in Program Semantics, Dominance as Program Semantics
  IMDEA Software Institute, Madrid, Spain. August 2012.
  
• Gradual Ownership Types
  Entropy Meeting, Programming Languages Group, Aarhus University. Aarhus, Denmark. December 2011.
  
• Scripting an IDE for DSL awareness
  Devoxx 2009. Antwerp, Belgium. November 2009.
  
• Clojure support in IntelliJ IDEA
  The Bay Area Clojure User Group meetup. San Francisco, CA, USA. June 2009.
  
• Cross-Language Development in IntelliJ IDEA
  JAX 2009. Mainz, Germany. April 2009.
  
• Cross-Language Development Experience on the JVM [Video]
  Devoxx 2008. Antwerp, Belgium. December 2008.