Address

Dmitriy Traytel
Department of Computer Science
University of Copenhagen
Sigurdsgade 41
2200 Copenhagen N, Denmark
Office: 2.14
Email: traytel di ku dk
PGP Key

Dmitriy Traytel

I am an associate professor at the University of Copenhagen (UCPH) since August 2020. I am part of (and currently head of) the Software, Data, People & Society (SDPS) section of UCPH's Department of Computer Science (DIKU). Before that I worked as a senior researcher (Oberassistent) in the Information Security Group led by David Basin at ETH Zürich. I completed my PhD at TU München under Tobias Nipkow's supervision in 2015. My research interests include logic, automata, runtime verification and monitoring, decision procedures, (co)induction and (co)recursion, and interactive theorem proving. Take a look at my (draft) publications, students I have (co)supervised / am (co)supervising, some tools I have (co)developed / am (co)developing, and scientific events I was involved in.

News

• I serve on the program committee for RV 2024. Send your best runtime verification papers!
• I serve on the program committee for ITP 2024. Send your best theorem proving papers!
• I have received the Sapere Aude: DFF Starting Grant from the Independent Research Fund Denmark (DFF) to work on formally verified data stream processing. I will be looking for a PhD student and a postdoctoral researcher starting in mid/end 2024.
• I serve on the program committee for FORTE 2024. Send your best papers in distributed systems!

Drafts

• Verified Time-Aware Stream Processing
  Rafael Castro Gonçalves Silva, DT

Publications

Journal Articles

• 2023
  Efficient Evaluation of Arbitrary Relational Calculus Queries
  Extended version of the ICDT 2022 paper
  Martin Raszyk, David Basin, Srđan Krstić, DT
  In Logical Methods in Computer Science, 19(4), 2023, doi.
• 2022
  Quotients of Bounded Natural Functors
  Extended version of the IJCAR 2020 paper
  Basil Fürer, Andreas Lochbihler, Joshua Schneider, DT
  In Logical Methods in Computer Science, 18(1), 2022, doi.
• 2021
  Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant
  Extended version of the CADE 2019 paper
  Andrei Popescu, DT
  In Journal of Automated Reasoning, 65(7), pp. 1027–1070, 2021 (published online: Aug 2021), doi.
• Scalable Online First-Order Monitoring
  Extended version of the RV 2018 paper
  Joshua Schneider, David Basin, Frederik Brix, Srđan Krstić, DT
  In International Journal on Software Tools for Technology Transfer, 23(2), pp. 185–208, 2021 (published online: Jun 2021), doi.
• A Taxonomy for Classifying Runtime Verification Tools
  Extended version of the RV 2018 paper
  Yliès Falcone, Srđan Krstić, Giles Reger, DT
  In International Journal on Software Tools for Technology Transfer, 23(2), pp. 255–284, 2021 (published online: May 2021), doi.
• 2020
  Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
  Extended version of the IJCAR 2018 paper
  Anders Schlichtkrull, Jasmin Blanchette, DT, Uwe Waldmann
  In Journal of Automated Reasoning, 64(7), pp. 1169–1195, 2020 (published online: Jun 2020), doi.
• 2019
  A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)
  César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Yliés Falcone, Adrian Francalanza, Srđan Krstić, João M. Lourenço, Dejan Nickovic, Gordon J. Pace, Jose Rufino, Julien Signoles, DT, Alexander Weiss
  In Formal Methods in System Design, 54(3), pp. 279–335, 2019 (published online: Nov 2019), doi.
• Almost Event-Rate Independent Monitoring
  Extended unified version of the TACAS 2017 and RV 2017 papers
  David Basin, Bhargav Bhatt, Srđan Krstić, DT
  In Formal Methods in System Design, 54(3), pp. 449–478, 2019 (published online: Feb 2019), doi.
• 2017
  Formal Languages, Formally and Coinductively
  Extended version of the FSCD 2016 paper
  DT
  In Logical Methods in Computer Science, 13(3), 2017, doi.
• 2016
  Soundness and Completeness Proofs by Coinductive Methods
  Extended version of the IJCAR 2014 paper
  Jasmin Christian Blanchette, Andrei Popescu, DT.
  In Journal of Automated Reasoning, 58(1), pp. 149–179, 2017 (published online: Oct 2016), doi.
• 2015
  Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
  Extended version of the ICFP 2013 paper
  DT, Tobias Nipkow
  In Journal of Functional Programming, 25, 2015, doi.

Conference Papers

• 2024
  Proactive Real-Time First-Order Enforcement
  François Hublet, Leonardo Lima, David Basin, Srđan Krstić, DT
  In Gurfinkel, A., Ganesh, V. (eds.) 36th International Conference on Computer Aided Verification (CAV 2024), Springer, 2024, to appear.
• Explainable Online Monitoring of Metric First-Order Temporal Logic
  Leonardo Lima, Jonathan Julián Huerta y Munive, DT
  In Finkbeiner, B., Kovács, L. (eds.) 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024), LNCS 14570, pp. 288–307, Springer, 2024, doi.
• 2023
  Correct and Efficient Policy Monitoring, a Retrospective
  Invited paper: David Basin was the invited author
  David Basin, Srđan Krstić, Joshua Schneider, DT
  In André, É, Jun, S. (eds.) 21st International Symposium on Automated Technology for Verification and Analysis (ATVA 2023), LNCS 14215, pp. 3–30, Springer, 2023, doi.
• Explainable Online Monitoring of Metric Temporal Logic
  Leonardo Lima, Andrei Herasimau, Martin Raszyk, DT, Simon Yuan
  In Sharygina, N., Sankaranarayanan, S. (eds.) 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), LNCS 13994, pp. 473–491, Springer, 2023, doi.
• Admissible Types-to-PERs Relativization in Higher-Order Logic
  Distinguished Paper Award
  Andrei Popescu, DT
  In Ahmed, A. (ed.) 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023), Article 42, pp. 42:1–42:32, ACM, 2023, doi.
• 2022
  VeriMon: A Formally Verified Monitoring Tool
  Invited paper: I was the invited author
  David Basin, Thibault Dardinier, Nico Hauser, Lukas Heimes, Jonathan Julián Huerta y Munive, Nicolas Kaletsch, Srđan Krstić, Emanuele Marsicano, Martin Raszyk, Joshua Schneider, Dawit Legesse Tirore, DT, Sheila Zingg
  In Seidl, H., Liu, Z., Pasareanu, C. (eds.) 19th International Colloquium on Theoretical Aspects of Computing (ICTAC 2022), LNCS 13572, pp. 1–6, Springer, 2022, doi
• Differential Testing of Pushdown Reachability with a Formally Verified Oracle
  Anders Schlichtkrull, Morten Konggaard Schou, Jiří Srba, DT
  In Griggio, A., Rungta, N. (eds.) 22nd International Conference on Formal Methods in Computer-Aided Design (FMCAD 2022), pp. 369–379, TU Wien Academic Press, 2022, doi
• Verified First-Order Monitoring with Recursive Rules
  Sheila Zingg, Srđan Krstić, Martin Raszyk, Joshua Schneider, DT
  In Fisman, D., Rosu, G. (eds.) 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), LNCS 13244, pp. 236–253, Springer, 2022, doi.
• Practical Relational Calculus Query Evaluation
  Martin Raszyk, David Basin, Srđan Krstić, DT
  In Olteanu, D., Vortmeier, N. (eds.) 25th International Conference on Database Theory (ICDT 2022), , LIPIcs 220, pp. 11:1–11:21, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2022, doi
• 2021
  Verified Progress Tracking for Timely Dataflow
  Matthias Brun, Sára Decova, Andrea Lattuada, DT
  In Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021), LIPIcs 193, pp. 10:1–10:20, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2021, doi.
• 2020
  Multi-Head Monitoring of Metric Dynamic Logic
  Martin Raszyk, David Basin, DT
  In Van Hung, D., Sokolsky, O. (eds.) 18th International Symposium on Automated Technology for Verification and Analysis (ATVA 2020), LNCS 12302, pp. 233–250, Springer, 2020, doi.
• Quotients of Bounded Natural Functors
  Basil Fürer, Andreas Lochbihler, Joshua Schneider, DT
  In Peltier, N., Sofronie-Stokkermans, V. (eds.) 10th International Joint Conference on Automated Reasoning (IJCAR 2020), LNCS 12167, pp. 58–78, Springer, 2020, doi.
• A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
  David Basin, Thibault Dardinier, Lukas Heimes, Srđan Krstić, Martin Raszyk, Joshua Schneider, DT
  In Peltier, N., Sofronie-Stokkermans, V. (eds.) 10th International Joint Conference on Automated Reasoning (IJCAR 2020), LNCS 12166, pp. 432–453, Springer, 2020, doi.
• 2019
  A Formally Verified Monitor for Metric First-Order Temporal Logic
  Joshua Schneider, David Basin, Srđan Krstić, DT
  In Finkbeiner, B., Mariani, L. (eds.) 19th International Conference on Runtime Verification (RV 2019), LNCS 11757, pp. 310–328, Springer, 2019, doi.
• Multi-Head Monitoring of Metric Temporal Logic
  Martin Raszyk, David Basin, Srđan Krstić, DT
  In Chen, Y.-F., Cheng, C.-H., and Esparza, J. (eds.) 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), LNCS 11781, 151–170, Springer, 2019, doi.
• Adaptive Online First-Order Monitoring
  Joshua Schneider, David Basin, Frederik Brix, Srđan Krstić, DT
  In Chen, Y.-F., Cheng, C.-H., and Esparza, J. (eds.) 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), LNCS 11781, 133–150, Springer, 2019, doi.
• Generic Authenticated Data Structures, Formally
  Matthias Brun, DT
  In Tolmach, A., Harrison, J., O'Leary, J. (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019), LIPIcs 141, pp. 10:1–10:18, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019, doi.
• A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
  Andrei Popecsu, DT
  In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 442–461, Springer, 2019, doi.
• From Nondeterministic to Multi-Head Deterministic Finite-State Transducers
  Martin Raszyk, David Basin, DT
  In Baier, C. (ed.) 46th International Colloquium on Automata, Languages and Programming (ICALP 2019), LIPIcs 132, pp. 127:1–127:14, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019, doi.
• Bindings as Bounded Natural Functors
  Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, DT
  In Weirich, S. (ed.) 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), Article 22, pp. 22:1–22:34, ACM, 2019, doi.
• A Verified Prover Based on Ordered Resolution
  Anders Schlichtkrull, Jasmin Christian Blanchette, DT
  In Mahboubi, A., Myreen, M. O. (eds.) 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), 152–165, ACM, 2019, doi.
• 2018
  Scalable Online First-Order Monitoring
  Joshua Schneider, David Basin, Frederik Brix, Srđan Krstić, DT
  In Colombo, C., Leucker, M. (eds.) 18th International Conference on Runtime Verification (RV 2018), LNCS 11237, pp. 353–371, Springer, 2018, doi.
• A Taxonomy for Classifying Runtime Verification Tools
  Yliès Falcone, Srđan Krstić, Giles Reger, DT
  In Colombo, C., Leucker, M. (eds.) 18th International Conference on Runtime Verification (RV 2018), LNCS 11237, pp. 241–262, Springer, 2018, doi.
• Optimal Proofs for Linear Temporal Logic on Lasso Words
  Distinguished Paper Award
  David Basin, Bhargav Bhatt, DT
  In Lahiri, S., Wang, C. (eds.) 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), LNCS 11138, pp. 37–55, Springer, 2018, doi.
• Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
  Anders Schlichtkrull, Jasmin Christian Blanchette, DT, Uwe Waldmann
  In Galmiche, D., Schulz, S., Sebastiani, S. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018), LNCS 10900, pp. 89–107, Springer, 2018, doi.
• 2017
  Almost Event-Rate Independent Monitoring of Metric Dynamic Logic
  David Basin, Srđan Krstić, DT
  In Lahiri, S., Reger, G. (eds.) 17th International Conference on Runtime Verification (RV 2017), LNCS 10548, pp. 85–102, Springer, 2017, doi.
• Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
  Invited paper: Jasmin Christian Blanchette was the invited author
  Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, DT
  In Dixon, C., Finger, M. (eds.) 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), LNCS 10483, pp. 3–21, Springer, 2017, doi.
• Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
  Jasmin Christian Blanchette, Mathias Fleury, DT.
  In Miller, D. (ed.) 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), LIPIcs 84, pp. 11:1–11:18, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2017, doi.
• Foundational Nonuniform (Co)datatypes in Higher-Order Logic
  Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, DT
  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), 1–12, IEEE, 2017, doi.
• Almost Event-Rate Independent Monitoring of Metric Temporal Logic
  David Basin, Bhargav Bhatt, DT
  In Legay, A., Margaria, T. (eds.) 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), LNCS 10206, pp. 94–112, Springer, 2017, doi.
• Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants
  Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, DT
  In Yang, H. (ed.) 26th European Symposium on Programming (ESOP 2017), LNCS 10201, pp. 111–140, Springer, 2017, doi.
• 2016
  Formal Languages, Formally and Coinductively
  Best Student Paper Award
  DT.
  In Kesner, D., Pientka, B. (eds.) 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), LIPIcs 52, pp. 31:1–31:17, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016, doi.
• 2015
  A Coalgebraic Decision Procedure for WS1S
  DT.
  In Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), LIPIcs 41, pp. 487–503, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015, doi.
• A Formalized Hierarchy of Probabilistic System Types (Proof Pearl)
  Johannes Hölzl, Andreas Lochbihler, DT
  In Zhang, X., Urban, C. (eds.) 6th International Conference on Interactive Theorem Proving (ITP 2015), LNCS 9236, pp. 203–220, Springer, 2015, doi.
• Foundational Extensible Corecursion
  A Proof Assistant Perspective
  Jasmin Christian Blanchette, Andrei Popescu, DT
  In Reppy, J. (ed.) 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), pp. 192–204, ACM, 2015, doi.
• Witnessing (Co)datatypes
  Jasmin Christian Blanchette, Andrei Popescu, DT
  In Vitek, J. (ed.) 24th European Symposium on Programming (ESOP 2015), LNCS 9032, pp. 359–382, Springer, 2015, doi.
• 2014
  Experience Report: The Next 1100 Haskell Programmers
  Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, DT
  In Swierstra, W. (ed.) 2014 ACM SIGPLAN Symposium on Haskell (Haskell 2014), ACM, 2014, doi.
• Cardinals in Isabelle/HOL
  Jasmin Christian Blanchette, Andrei Popescu, DT
  In Klein, G., Gamboa, R. (eds.) 5th International Conference on Interactive Theorem Proving (ITP 2014), LNCS 8558, pp. 111–127, Springer, 2014, doi.
• Truly Modular (Co)datatypes for Isabelle/HOL
  Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, DT
  In Klein, G., Gamboa, R. (eds.) 5th International Conference on Interactive Theorem Proving (ITP 2014), LNCS 8558, pp. 93–110, Springer, 2014, doi.
• Unified Classical Logic Completeness: A Coinductive Pearl
  Jasmin Christian Blanchette, Andrei Popescu, DT
  In Demri, S., Kapur, D., Weidenbach, C. (eds) 7th International Joint Conference on Automated Reasoning (IJCAR 2014), LNCS 8562, pp. 46–60, Springer, 2014, doi.
• Unified Decision Procedures for Regular Expression Equivalence
  Tobias Nipkow, DT
  In Klein, G., Gamboa, R. (eds.) 5th International Conference on Interactive Theorem Proving (ITP 2014), LNCS 8558, pp. 450–466, Springer, 2014, doi.
• 2013
  Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
  Functional Pearl
  DT, Tobias Nipkow
  In Morrisett, G., Uustalu, T. (eds.) 18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013), pp. 3–12, ACM, 2013, doi.
• 2012
  Foundational, Compositional (Co)datatypes for Higher-Order Logic
  DT, Andrei Popescu, Jasmin Christian Blanchette
  In 27th Annual IEEE Symposium on Logic in Computer Science (LICS 2012), pp. 596–605, IEEE, 2012, doi.
• 2011
  Extending Hindley-Milner Type Inference with Coercive Structural Subtyping
  DT, Stefan Berghofer, Tobias Nipkow
  In Yang, H. (ed.) 9th Asian Symposium on Program Languages and Systems (APLAS 2011), LNCS 7078, pp. 89–104, Springer, 2011, doi.

Workshop Papers

• 2017
  A Report of ARCADE 2017
  Giles Reger, DT
  In 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2017).
• Aerial: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties
  Tool Paper
  David Basin, Srđan Krstić, DT
  In International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES 2017).
• Conditional Parametricity in Isabelle/HOL
  Extended abstract
  Jan Gilcher, Andreas Lochbihler, DT
  In Poster Session at TABLEAUX/FroCoS/ITP 2017.
• 2016
  Friends with Benefits: Implementing Foundational Corecursion in Proof Assistants (Extended Abstract)
  Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, DT
  In Isabelle Workshop 2016.
• 2015
  Derivatives of WS1S Formulas
  DT
  In Frontiers of Formal Methods 2015.
• 2014
  Primitively (Co)recursive Definitions for Isabelle/HOL
  Lorenz Panny, Jasmin Christian Blanchette, DT
  In Isabelle Workshop 2014.

Theses

Ph.D.

Formalizing Symbolic Decision Procedures for Regular Languages [official copy]

M.Sc.

A Category Theory Based (Co)datatype Package for Isabelle/HOL

B.Sc.

Extension of a Type Inference Algorithm with Coercive Subtyping

Supervision

Current

• PhD
  Rafael Castro G. Silva (Ph.D.)
  Trustworthy Stream Processing.
• Leonardo Lima (Ph.D.)
  Explainable Runtime Monitoring.
• Lennard Reese (Ph.D.)
  Runtime Monitoring for Proof Assistants.
• MSc
  Mathias Rabing (M.Sc.)
  Nonuniform (Co)datatypes in Isabelle/HOL.
• BSc
  Matthias Lott (B.Sc., cosupervisor: Srđan Krstić)
  Temporal Data Golf.

Past

• postdoc
  Jonathan Julian Huerta y Munive (postdoc)
  Trustworthy Runtime Monitoring.
• PhD
  Joshua Schneider (Ph.D., cosupervisors: David Basin and Srđan Krstić)
  Scalable and Trustworthy Monitoring.
• Martin Raszyk (Ph.D., cosupervisor: David Basin)
  Efficient, Expressive, and Verified Temporal Query Evaluation.
• MSc
  Christian Franck (M.Sc., cosupervisor: Lennard Reese)
  Propagating Negative Information in Streaming First-Order Monitoring.
• Karen Qvist Larsen and Nanna Munk Berg (M.Sc., cosupervisor: Rafael Castro G. Silva)
  Aggregations, Sharing, and Recursion in Streaming First-Order Monitoring.
• Sebastian Paarmann (M.Sc. project outside the course scope)
  Formalizing Π4 in Isabelle/HOL.
• Thorbjørn Bülow Bringgaard (M.Sc. project outside the course scope)
  Verified Log Parsing and a General Time Domain for VeriMon.
• Lennard Reese (M.Sc., cosupervisor: Rafael Castro G. Silva)
  Efficient Streaming Algorithms for Metric First-Order Temporal Logic in Timely Dataflow.
• Tobias Larsen (M.Sc., cosupervisor: Joshua Schneider)
  Database-style Indices in a Formally Verified Runtime Monitor.
• Mathias Rabing (M.Sc. project outside the course scope, cosupervisor: Joshua Schneider)
  Formalizing Gödel's Incompleteness Theorems for Intuitionistic Logic in Isabelle/HOL.
• Jan van Brügge (M.Sc., cosupervisor: Lukas Stevens)
  Towards Binding-Aware Datatypes For Isabelle/HOL.
• Sheila Zingg (M.Sc., cosupervisor: Joshua Schneider)
  Verified Evaluation of Recursive Expressions in Metric First-Order Dynamic Logic.
• Dawit Legesse Tirore (M.Sc. project outside the course scope, cosupervisor: Martin Raszyk)
  Verified Rewriting of Metric First-Order Temporal Logic Formulas.
• Matthias Brun (Student Research Assistant)
  Verified Stream Processing and Analytics.
• François Hublet (Semester project, cosupervisors: Martin Raszyk and Srđan Krstić)
  Monitoring Unsafe First-order Formulas.
• Sara Decova (M.Sc., cosupervisor: Andrea Lattuada)
  Modeling and Verification of the Timely Dataflow Progress Tracking Protocol.
• Sarah Plocher (M.Sc., cosupervisor: Srđan Krstić)
  From StreamingSQL to MFOTL.
• Thibault Dardinier (Direct doctorate research project, cosupervisor: Martin Raszyk)
  Formalizing Multiway-Join Algorithms in Isabelle/HOL.
• Pascal Stoop (M.Sc.)
  Binding Datatypes in Isabelle/HOL.
• Frederik Brix (M.Sc., cosupervisors: Srđan Krstić and Joshua Schneider)
  Adaptive Online Monitoring.
• Galina Peycheva (M.Sc., cosupervisors: John Liagouris and Frank McSherry)
  Real-time Verification of Datacenter Security Policies via Online Log Analysis.
• Tom Sydney Kerckhove (M.Sc.)
  Signature Inference for QuickSpec.
• Fabian Meier (M.Sc.)
  Non-uniform Datatypes in Isabelle/HOL.
• Anders Schlichtkrull (M.Sc., main supervisors: Jørgen Villadsen, Jasmin Blanchette)
  Formalization of Resolution Calculus in Isabelle.
• Aymeric Bouzy (M.Sc. intern, cosupervisor: Jasmin Blanchette)
  Non-primitive Corecursion Support in Isabelle/HOL.
• Mathias Fleury (M.Sc., main supervisor: Jasmin Blanchette)
  Formalization of Ground Inference Systems.
• BSc
  Helene Møller-Jensen and Johannes Rosendal (B.Sc.)
  A User-Friendly Frontend for RC-Eval.
• Olivia Sommer Nørgaard (B.Sc. project outside the course scope)
  A Collection of Relational Calculus Queries for a Database Course
• Polina Ziboreva (B.Sc.)
  Anomaly Detection for Data Quality: Rule-based vs. Model-based
• Hróbjartur Höskuldsson (B.Sc.)
  Monitoring the EU AI Act with Metric First-order Temporal Logic.
• Johannes Meyer (B.Sc., cosupervisor: Joshua Schneider)
  Towards a Formalization of Gödel's Incompleteness Theorems for Intuitionistic Logic
• Emma Pind Hansen (B.Sc.)
  Streaming Algorithms for Metric First-Order Temporal Operators
• Jonathan Rappl (B.Sc., cosupervisor: Joshua Schneider)
  Verifying VeriMon's Event Parser.
• Valeria Jannelli (B.Sc., cosupervisor: Srđan Krstić)
  A White-Box Parallel Monitor for Metric First-Order Temporal Logic.
• Roman Angehrn (B.Sc., cosupervisor: Joshua Schneider)
  Formalizing Higher-Order Pattern Unification in Isabelle/HOL.
• Andrei Herasimau (B.Sc., cosupervisor: Martin Raszyk)
  Formalizing Explanations for Metric Temporal Logics.
• Lukas Heimes (B.Sc., cosupervisor: Joshua Schneider)
  Extending and Optimizing a Verified Monitor for Metric First-Order Temporal Logic.
• Gabriel Giamarchi (B.Sc.)
  Formalizing Automata Learning in Isabelle/HOL.
• Simon Yuan (B.Sc., cosupervisor: Martin Raszyk)
  Explaining Monitoring Verdicts for Metric Dynamic Logic.
• Ben Fiedler (B.Sc.)
  Formalizing Distributed Snapshots in Isabelle/HOL.
• Basil Fürer (B.Sc., cosupervisor: Joshua Schneider)
  Functor-Preserving Quotients in Isabelle/HOL.
• Matthias Roshardt (B.Sc.)
  Generalized Functor Composition in Isabelle/HOL.
• Christian Fania (B.Sc., cosupervisors: Srđan Krstić and Joshua Schneider)
  Self-Adaptive Online Monitoring.
• Matthias Brun (B.Sc.)
  Authenticated Data Structures in Isabelle/HOL.
• Jan Gilcher (B.Sc., cosupervisor: Andreas Lochbihler)
  Conditional Parametricity in Isabelle/HOL.
• Julian Biendarra (B.Sc., cosupervisor: Lars Hupel)
  Functor-Preserving Type Definitions.
• Matthias Franze (B.Sc.)
  A Purely-Functional, Proof-Producing, Incremental Algorithm for the Congruence Closure.
• Martin Desharnais (B.Eng., cosupervisor: Jasmin Blanchette)
  Formalizing Types and Programming Languages.
• Lorenz Panny (B.Sc., cosupervisor: Jasmin Blanchette)
  Primitively (Co)recursive Function Definitions.

Tools

Current

• Aerial—an almost event-rate independent monitor for metric temporal logic
• Isabelle—a generic proof assistant
• VeriMon—a formally verified monitor for metric first-order dynamic logic
• WhyMon—explaining online monitoring verdicts for metric first-order temporal logic

Past

• Explanator—explaining offline monitoring verdicts for linear temporal logic on lasso words
• Explanator2—explaining online monitoring verdicts for metric temporal logic
• Hecke—a GAP 4 package for calculating decomposition matrices of Hecke algebras of the symmetric groups and q-Schur algebras
• MonaCo—a symbolic coalgebraic decision procedure for weak monadic second-order logic of one successor (WS1S)
• POTATOES—a small operating system for x86 platforms

Events

Forthcoming

• RV 2024 (PC member)
• ITP 2024 (PC member)
• FORTE 2024 (PC member)

Past

• CPP 2024 (Conference Chair)
• FroCoS 2023 (PC Member)
• RV 2023 (PC Member)
• CPP 2023 (Conference Chair)
• ICTAC 2022 (Invited Speaker)
• RV 2022 (PC member)
• CPP 2022 (PC member)
• RV 2021 (PC member)
• RV 2020 (PC member)
• CPP 2020 (PC member)
• POPL Artifact Evaluation 2020 (AEC member)
• TABLEAUX 2019 (PC member)
• RV-CuBES 2017 Workshop (PC member)
• ARCADE Workshop (PC chair) [proceedings]
• Isabelle Tutorial @ ICFP 2017 (Organizer and Lecturer)
• Isabelle Tutorial @ CADE-26 (Organizer and Lecturer)
• CALCO 2017 Early Ideas (PC member)
• PUMA/RiSE Workshop 2014 (Organizer)
• PUMA/RiSE Workshop 2012 (Organizer)

© 2011–2024 by Dmitriy Traytel