Address
Dmitriy Traytel
Department of Computer Science
University of Copenhagen
Sigurdsgade 41
2200 Copenhagen N, Denmark
Office: 2.15
Email: traytel di ku
dk
PGP Key
Dmitriy Traytel
Starting from August 2020, I work as an associate professor at the University of Copenhagen (UCPH). I am part 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 in 2015 at TU München under
Tobias Nipkow's supervision.
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
Drafts
Publications
Journal Articles
2020
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, 2020, accepted with minor revisions.

Scalable Online FirstOrder 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, 2020, accepted with minor revisions.

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, 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 EventRate 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

2020
MultiHead 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., SofronieStokkermans, 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 FirstOrder Dynamic Logic
David Basin, Thibault Dardinier, Lukas Heimes, Srđan Krstić, Martin Raszyk, Joshua Schneider, DT
In Peltier, N., SofronieStokkermans, 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 FirstOrder 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.

MultiHead 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 FirstOrder 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 Conference on Interactive Theorem Proving (ITP 2019), LIPIcs 141, pp. 10:1–10:18, Schloss Dagstuhl–LeibnizZentrum 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 (CADE27), LNCS 11716, pp. 442–461, Springer, 2019, doi.

From Nondeterministic to MultiHead Deterministic FiniteState 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–LeibnizZentrum 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 FirstOrder 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 EventRate 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 HigherOrder 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–LeibnizZentrum fuer Informatik, 2017, doi.

Foundational Nonuniform (Co)datatypes in HigherOrder 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 EventRate 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–LeibnizZentrum 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–LeibnizZentrum 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 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 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 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 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 HigherOrder 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 HindleyMilner 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 EventRate 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 (RVCuBES 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
Student (Co)supervision
Current
 Dawit Legesse Tirore (M.Sc. project outside the course scope, cosupervisor: Martin Raszyk)
Verified Rewriting of MFOTL Formulas.
 Stefan Zemljic (B.Sc., cosupervisor: Joshua Schneider, Srđan Krstić, and Reto Märki)
Monitoring SubLedger Accounting with Metric FirstOrder Temporal Logic.
 Valeria Jannelli (B.Sc., cosupervisor: Srđan Krstić)
A WhiteBox Parallel Monitor for Metric FirstOrder Temporal Logic.
 Martin Raszyk (Ph.D., cosupervisor: David Basin)
Big Data Monitoring.
 Joshua Schneider (Ph.D., cosupervisors: David Basin and Srđan Krstić)
Monitoring at Any Cost.
Past
 Roman Angehrn (B.Sc., cosupervisor: Joshua Schneider)
Formalizing HigherOrder Pattern Unification in Isabelle/HOL.
 Matthias Brun (Student Research Assistant)
Verified Stream Processing and Analytics.
 François Hublet (Semester project, cosupervisors: Martin Raszyk and Srđan Krstić)
Monitoring Unsafe Firstorder Formulas.
 Sara Decova (M.Sc., cosupervisor: Andrea Lattuada)
Modeling and Verification of the Timely Dataflow Progress Tracking Protocol.
 Andrei Herasimau (B.Sc., cosupervisor: Martin Raszyk)
Formalizing Explanations for Metric Temporal Logics.
 Sarah Plocher (M.Sc., cosupervisor: Srđan Krstić)
From StreamingSQL to MFOTL.
 Lukas Heimes (B.Sc., cosupervisor: Joshua Schneider)
Extending and Optimizing a Verified Monitor for Metric FirstOrder Temporal Logic.
 Gabriel Giamarchi (B.Sc.)
Formalizing Automata Learning in Isabelle/HOL.
 Thibault Dardinier (Direct doctorate research project, cosupervisor: Martin Raszyk)
Formalizing MultiwayJoin Algorithms 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)
FunctorPreserving 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)
SelfAdaptive Online Monitoring.
 Matthias Brun (B.Sc.)
Authenticated Data Structures 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)
Realtime Verification of Datacenter Security Policies via Online Log Analysis.
 Tom Sydney Kerckhove (M.Sc.)
Signature Inference for QuickSpec.
 Jan Gilcher (B.Sc., cosupervisor: Andreas Lochbihler)
Conditional Parametricity in Isabelle/HOL.
 Fabian Meier (M.Sc.)
Nonuniform Datatypes in Isabelle/HOL.
 Julian Biendarra (B.Sc., cosupervisor: Lars Hupel)
FunctorPreserving Type Definitions.
 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)
Nonprimitive Corecursion Support in Isabelle/HOL.
 Mathias Fleury (M.Sc. intern, main supervisor: Jasmin Blanchette)
Formalization of Ground Inference Systems.
 Matthias Franze (B.Sc.)
A PurelyFunctional, ProofProducing, 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 eventrate independent monitor for metric temporal logic

Explanator—explaining monitoring verdicts for linear temporal logic on lasso words

Isabelle—a generic proof
assistant

VeriMon—a formally verified monitor for metric firstorder dynamic logic
Past

Hecke—a GAP 4 package for calculating
decomposition matrices of Hecke algebras of the symmetric groups and qSchur
algebras

MonaCo—a symbolic coalgebraic decision procedure for
weak monadic secondorder logic of one successor (WS1S)

POTATOES—a small
operating system for x86 platforms
Events
Forthcoming
Past
© 2011–2021 by Dmitriy Traytel