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
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
TimelyMon: A Streaming Parallel First-Order Monitor
Tool Paper
Lennard Reese, Rafael Castro G. Silva, DT
In Abraham, E., Abbas, H., (eds.) 24th International Conference on Runtime Verification (RV 2024), Springer, 2024, to appear.
- WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts
Tool Paper
Leonardo Lima, Jonathan Julián Huerta y Munive, DT
In Akshay, S., Niemetz, A., Sankaranarayanan, S., (eds.) 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA 2024), Springer, 2024, to appear.
-
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), LNCS 14682, pp. 156–181, Springer, 2024, doi.
-
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
postdoc
Asta Halkjær From (postdoc)
Trustworthy Stream Processing.
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.
BSc
Rosa Marie Haslund Meyer (B.Sc., cosupervisor: Leonardo Lima)
Explainable Monitoring of Regular Expressions
- William Marosi (B.Sc., cosupervisor: Lennard Reese)
A Benchmark for First-Order Runtime Monitoring Tools
- Andreas Carlson (B.Sc., cosupervisor: Lennard Reese)
Differential Evaluation in a Streaming Monitor
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
Janus Jonatan Hannesarson (M.Sc., cosupervisor: Lennard Reese)
Efficient Temporal Aggregations in TimelyMon
- Mathias Rabing (M.Sc.)
Nonuniform (Co)datatypes in Isabelle/HOL.
- 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
Bastian Frank Nielsen (B.Sc., cosupervisor: Lennard Reese)
Enhancing TimelyMon with JSON Processing
- Matthias Lott (B.Sc., cosupervisor: Srđan Krstić)
Temporal Data Golf.
- 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
-
Isabelle—a generic proof
assistant
-
TimelyMon—a scalable streaming first-order monitor for metric first-order temporal logic
-
VeriMon—a formally verified monitor for metric first-order dynamic logic
-
WhyMon—explaining online monitoring verdicts for metric first-order temporal logic
Past
-
Aerial—an almost event-rate independent monitor for metric temporal logic
-
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
Past
© 2011–2024 by Dmitriy Traytel