Talks

• Interactive Formal Verification
  January 12, 2024. Docentship Lecture. Uppsala University, Uppsala (Sweden).
• Sustainable Compiler Verification
  January 12, 2024. UU Workshop on Cybersecurity, Uppsala (Sweden).
• Conservative Definitions for Higher-order Logic with Overloading
  May 24, 2021. TCS Seminar, KTH, Stockholm (Sweden). Talk given online.
• The International Satisfiability Modulo Theories Competition (SMT-COMP)
  February 18, 2019. Advancing Verification Competitions as a Scientific Method, Lorentz Center, Leiden (Netherlands).
• 13th International Satisfiability Modulo Theories Competition - SMT-COMP 2018
  July 14, 2018. FLoC Olympic Games Award Ceremony, FLoC 2018, Oxford (UK).
• 13th International Satisfiability Modulo Theories Competition - SMT-COMP 2018
  July 13, 2018. SMT 2018, Oxford (UK).
• Satisfiability Modulo Theories and the SMT Competition
  March 29, 2017. Concurrency Seminar, Uppsala (Sweden).
• 11th International Satisfiability Modulo Theories Competition - SMT-COMP 2016
  July 2, 2016. SMT 2016, Coimbra (Portugal).
• Scrambling and Descrambling SMT-LIB Benchmarks
  July 1, 2016. SMT 2016, Coimbra (Portugal).
• Resource Monitoring for Poly/ML Processes
  September 3, 2015. ACM SIGPLAN Workshop on ML, Vancouver (Canada).
• A Generic Process Calculus Approach to Relaxed-Memory Consistency
  February 23, 2015. UPMARC Workshop on Memory Models (MM'15), Uppsala (Sweden).
• Integrating SAT, QBF and SMT Solvers with Interactive Theorem Provers
  Watch slides online or download offline presentation (59 MB, Windows and Mac only).
  October 9, 2013. Dagstuhl Seminar 13411: Deduction and Arithmetic, Schloss Dagstuhl (Germany).
• C/C++ Concurrency: Formalization and Model Finding
  September 25, 2013. Informal Presentation, RP 2013, Uppsala (Sweden).
• Interactive Verification of Relaxed-Memory Concurrency
  September 17, 2013. UPMARC Scientific Advisory Meeting, Uppsala (Sweden).
• The C/C++ Memory Model: Overview and Formalization
  May 29, 2013. UPMARC Workshop on Verification of Concurrent C Programs, Uppsala (Sweden).
• Interactive Verification of Relaxed-Memory Concurrency
  February 27, 2013. UPMARC Winter Meeting, Uppsala (Sweden).
• Making Formal Methods into Normal Methods
  September 20, 2012. Uppsala University, Uppsala (Sweden).
• Satisfiability Modulo Theories
  January 31, 2012. Verification of Erlang Programs Day, Uppsala (Sweden).
• Satisfiability Modulo Theories
  January 20, 2012. Mobility Seminar, Uppsala (Sweden).
• Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL
  Watch slides online or download offline presentation (22 MB, Windows and Mac only).
  December 8, 2011. CPP 2011, Kenting (Taiwan).
• Independent Proof Reconstruction for Z3: An Overview
  Watch slides online or download offline presentation (49 MB, Windows and Mac only).
  November 3, 2011. Z3 Special Interest Group Meeting, Microsoft Research, Cambridge (UK).
• Integrating SAT, QBF and SMT Solvers with Interactive Theorem Provers
  Watch slides online or download offline presentation (72 MB, Windows and Mac only).
  September 14, 2011. Department of Information Technology, Uppsala University, Uppsala (Sweden).
• Validating QBF Validity in HOL4   Demo
  August 25, 2011. ITP 2011, Berg en Dal (Netherlands). Talk given by Ramana Kumar.
• Designing Proof Formats: A User's Perspective
  August 1, 2011. PxTP 2011, Wrocław (Poland). Talk given jointly with Sascha Böhme.
• Validating QBF Validity in HOL4
  March 15, 2011. ARG Lunch, University of Cambridge (UK).
• Integrating SAT, QBF and SMT Solvers with Interactive Theorem Provers
  Watch slides online or download offline presentation (78 MB, Windows and Mac only).
  January 12, 2011. FoSS Seminar, University of Sussex, Brighton (UK).
• Integrating SAT, QBF and SMT Solvers with Interactive Theorem Provers
  Watch slides online or download offline presentation (77 MB, Windows and Mac only).
  August 11, 2010. TEITP 2010, Cambridge (UK).
• Validating QBF Invalidity in HOL4
  July 14, 2010. ITP 2010, Edinburgh (UK).
• Validating QBF Invalidity in HOL4
  July 2, 2010. TU München (Germany).
• Validating QBF Invalidity in HOL4
  June 1, 2010. ARG Lunch, University of Cambridge (UK).
• Integration of SMT Solvers with ITPs - There and Back Again
  May 7, 2010. University of Sheffield (UK).
• Integration of SMT Solvers with ITPs - There and Back Again
  March 2, 2010. ARG Lunch, University of Cambridge (UK).
• SMT Solvers: New Oracles for the HOL Theorem Prover
  November 17, 2009. ARG Lunch, University of Cambridge (UK).
• SMT Solvers: New Oracles for the HOL Theorem Prover
  November 2, 2009. VSTTE 2009, Eindhoven (Netherlands).
• Integrating SAT and SMT Solvers with Interactive Theorem Provers
  September 10, 2009. TypiCal, École Polytechnique, Paris (France).
• Finite Model Generation, Proof-Producing SAT Solvers, and Satisfiability Modulo Theories
  February 3, 2009. ARG Lunch, University of Cambridge (UK).
• SAT-based Finite Model Generation for Higher-Order Logic
  October 9, 2008. Thesis defense, TU München (Germany).
• Towards A Formal Semantics for C++ Types
  March 7, 2008. Digital Security Lunch Colloquium, Radboud University Nijmegen (Netherlands).
• Isabelle/HOL: Selected Features and Recent Improvements
  February 20, 2007. Security of Systems Group, Radboud University Nijmegen (Netherlands).
• Efficiently Checking Propositional Resolution Proofs in Isabelle/HOL
  November 12, 2006. IWIL'06, Phnom Penh (Cambodia).
• Isabelle/HOL: Integrated Theorem Proving
  April 10, 2006. Cooperation of Deduction Tools Day, Loria, Nancy (France).
• Integrating a SAT Solver with Isabelle/HOL
  March 6, 2006. First Munich-Nancy Workshop on Decision Procedures for Theorem Provers, TU München (Germany).
• A SAT-based Sudoku Solver
  December 3, 2005. LPAR 2005, Montego Bay (Jamaica).
• A SAT-based Sudoku Solver
  November 23, 2005. Club2, TU München (Germany).
• Using a SAT Solver as a Fast Decision Procedure for Propositional Logic in an LCF-style Theorem Prover
  August 23, 2005. TPHOLs 2005, Oxford (UK). A poster is available as well.
• SAT-based Finite Model Generation for Isabelle/HOL
  August 9, 2005. International Summer School Marktoberdorf, Marktoberdorf (Germany).
• Integrating a SAT Solver with an LCF-style Theorem Prover
  July 12, 2005. PDPAR'05, Edinburgh (UK).
• Bounded Model Generation for Isabelle/HOL
  March 23, 2005. Winterhütte, TU München (Germany).
• Integrating zChaff with Isabelle/HOL
  November 17, 2004. Club2, TU München (Germany).
• Satisfiability Modulo Theories
  November 11, 2004. Oberseminar Statische Analyse, TU München (Germany).
• Towards Mechanized Program Verification with Separation Logic
  September 21, 2004. CSL'04, Karpacz (Poland).
• Bounded Model Generation for Isabelle/HOL
  July 5, 2004. IJCAR 2004 - Workshop on Disproving, Cork (Ireland).
• Bounded Model Generation for Isabelle/HOL
  July 2, 2004. Club2, TU München (Germany).
• Finite Model Generation for Isabelle/HOL
  April 8, 2004. Spring School "Logic in Computer Science", Venice (Italy).
• Finite Model Generation for Isabelle/HOL
  March 3, 2004. Winterhütte, TU München (Germany).
• Finite Model Generation for Isabelle/HOL
  January 16, 2004. Club2, TU München (Germany).
• Constructively Characterizing Fold and Unfold
  August 26, 2003. LOPSTR 2003, Uppsala (Sweden).
• Separation Logic: A Hoare Logic for Pointer Programs
  July 23, 2003. Workshop Hoare-Logiken, TU & LMU München (Germany).
• Using Separation Logic to Verify Pointer Programs
  June 20, 2003. Club2, TU München (Germany).
• Program Transformations in Nuprl
  December 12, 2002. Arbeitstagung Bern - München, LMU München (Germany).
• Program Transformations in Nuprl
  July 26, 2002. Thesis defense, University of Wyoming, Laramie (USA).