Talks and Lectures

• Apalache Tutorial [pdf] at TLA+ Community Meeting 2024, co-located with Formal Methods 2024, Milan, Italy, September 2024.

• Finding Bugs for Fun & Profit with Informal Systems. A 4-hour workshop at Cosmoverse 2023. Istanbul, Türkiye, October 2023. Together with Tesnim Abdellatif and Josef Widder.

• Lectures on Quint, TLA+, and Apalache at the VTSA’23 summer school. VTSA23 Lecture material. Nancy, France, August 2023.

• Quint at Gateway to Cosmos. Prague, Czechia, June 2023.

• Apalache: symbolic model checker for TLA+. Extended version of the talk at TLA+ tutorial, co-located with DISC 2021. Online, October 2021.

• How TLA+ and Apalache Helped Us to Design the Tendermint Light Client. Interchain Conversations 2020. Online, December 2020.

• Model-based testing with TLA+ and Apalache, with Andrey Kupriyanov. TLA+ Community Event 2020. Online, October 2020.

• Type inference for TLA+ in Apalache, with Jure Kukovec. TLA+ Community Event 2020. Online, October 2020.

• Formal Spec and Model Checking of the Tendermint Blockchain Synchronization Protocol 2nd Workshop on Formal Methods for Blockchains. Online, July 2020.

• Tutorial at DISCOTEC/FORTE 2020, FORTE20 - pdfs + video. Online, June 2020.

• Tutorial at VMCAI Winter School 2020: VMCAI20 - pdf. Louisiana, USA, January 2020.

More talks to be found in my CV.