Address
Dmitriy Traytel
Institute of Information Security
Department of Computer Science
ETH Zürich
Universitätstrasse 6
8092 Zürich, Switzerland
Office: CNB F 107.2
Phone: +41 44 632 30 23
Email: traytel inf.ethz.ch
dblp GoogleScholar
Dmitriy Traytel
Starting from 2018, I am a senior researcher (Oberassistent) in
the Information Security Group led
by David Basin at ETH
Zürich. Before that I worked as a postdoctoral researcher in the same group. 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
 I am excited to serve on the program committees for TABLEAUX 2019 and CPP 2020. Send your best papers on automated reasoning and interactive theorem proving there!
 As part of the Formal Methods and Functional Programming course at ETH, which I am colecturing, Martin Raszyk organizes the next iteration of the Functional Programming Competition. The previous year's competition, which I have organized, can be found here.
 My (joint with David Basin and Bhargav Bhatt) paper Optimal Proofs for Linear Temporal Logic on Lasso Words received the ATVA 2018 Distinguished Paper award.
Drafts

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Extended version of the IJCAR 2018 paper
Anders Schlichtkrull, Jasmin Blanchette, DT, Uwe Waldmann

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
Publications
Journal Articles

2019
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, Springer, 2019, doi, to appear.

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

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), Springer, 2019, to appear.

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), Springer, 2019, to appear.

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), Springer, 2019, to appear.

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), Springer, 2019, to appear.

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), Springer, 2019, to appear.

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, 2019, to appear.

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), ACM, 2019, Article 22, pp. 22:1–22:34, 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), ACM, 2019, 152–165, 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), Springer, 2018, LNCS 11237, pp. 353–371, 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), Springer, 2018, LNCS 11237, pp. 241–262, 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), Springer, 2018, LNCS 11138, pp. 37–55, 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), Springer, 2018, LNCS 10900, pp. 89–107, 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), Springer, 2017, LNCS 10548, pp. 85–102, 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), Springer, 2017, LNCS 10483, pp. 3–21, 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), Springer, 2017, LNCS 10206, pp. 94–112, 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), Springer, 2017, LNCS 10201, pp. 111–140, 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), Springer, 2015, LNCS 9032, pp. 359–382, 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
 Thibault Dardinier (Direct doctorate research project, cosupervisor: Martin Raszyk)
Formalizing MultiwayJoin Algorithms in Isabelle/HOL.
 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)
FunctorPreserving Quotients in Isabelle/HOL.
 Matthias Roshardt (B.Sc.)
Generalized Functor Composition in Isabelle/HOL.
 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
 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

Isabelle—a generic proof
assistant

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

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

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