Personal information

No personal information available

Activities

Collapse all

Employment (4)

University of Copenhagen: Copenhagen, DK

2020-01-08 to present | Associate Professor (Computer Science)
Employment
Source: Self-asserted source
Dmitriy Traytel

ETH Zürich: Zurich, CH

2018-01-01 to 2020-07-31 | Senior researcher (Oberassistent) (Computer Science)
Employment
Source: Self-asserted source
Dmitriy Traytel

ETH Zürich: Zurich, ZH, CH

2015-08-01 to 2017-12-31 | Postdoctoral Researcher (Computer Science)
Employment
Source: Self-asserted source
Dmitriy Traytel

Technische Universität München: Munchen, Bayern, DE

2012-04-01 to 2015-07-31 | PhD student (Computer Science)
Employment
Source: Self-asserted source
Dmitriy Traytel

Works (50 of 59)

Items per page:
Page 1 of 2

TimelyMon

Runtime Verification - 24th International Conference, RV 2024, Proceedings
2025 | Conference paper | Author
DOI: 10.1007/978-3-031-74234-7_9
SOURCE-WORK-ID:

ff2e0837-33a2-4da2-a3d4-ba3e9417ff15

EID:

2-s2.0-85207657626

Part of ISBN: 9783031742330
Contributors: Lennard Reese; Rafael Castro G. Silva; Dmitriy Traytel
Source: check_circle
University of Copenhagen

Explainable Online Monitoring of Metric First-Order Temporal Logic

Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings
2024 | Conference paper | Author
DOI: 10.1007/978-3-031-57246-3_16
SOURCE-WORK-ID:

6bc14535-b25b-4378-b1fa-bca2c8214824

EID:

2-s2.0-85192166399

Part of ISBN: 9783031572456
Contributors: Leonardo Lima; Jonathan Julián Huerta y Munive; Dmitriy Traytel
Source: check_circle
University of Copenhagen

Proactive Real-Time First-Order Enforcement

Lecture Notes in Computer Science
2024 | Book chapter
DOI: 10.1007/978-3-031-65630-9_8
Part of ISBN: 9783031656293
Part of ISBN: 9783031656309
Part of ISSN: 0302-9743
Part of ISSN: 1611-3349
Contributors: François Hublet; Leonardo Lima; David Basin; Srđan Krstić; Dmitriy Traytel
Source: Self-asserted source
Dmitriy Traytel

Admissible Types-to-PERs Relativization in Higher-Order Logic

Proceedings of the ACM on Programming Languages
2023 | Journal article | Author
DOI: 10.1145/3571235
SOURCE-WORK-ID:

1fb8d52e-5c88-4079-987f-29f7fd01dc90

EID:

2-s2.0-85146578874
Contributors: Andrei Popescu; Dmitriy Traytel
Source: check_circle
University of Copenhagen

Correct and Efficient Policy Monitoring, a Retrospective

Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings
2023 | Conference paper | Author
DOI: 10.1007/978-3-031-45329-8_1
SOURCE-WORK-ID:

5933e56a-6cd9-48d1-9917-eb94c29a819e

EID:

2-s2.0-85175964999

Part of ISBN: 9783031453281
Contributors: David Basin; Srđan Krstić; Joshua Schneider; Dmitriy Traytel
Source: check_circle
University of Copenhagen

Efficient Evaluation of Arbitrary Relational Calculus Queries

Logical Methods in Computer Science
2023 | Journal article | Author
DOI: 10.46298/lmcs-19(4:38)2023
SOURCE-WORK-ID:

a995b04f-983d-40dc-b500-bc79e29fe6c1

EID:

2-s2.0-85180616843
Contributors: Martin Raszyk; David Basin; Srdan Krstić; Dmitriy Traytel
Source: check_circle
University of Copenhagen

Explainable Online Monitoring of Metric Temporal Logic

Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings
2023 | Conference paper | Author
DOI: 10.1007/978-3-031-30820-8_28
SOURCE-WORK-ID:

73375064-9f45-4748-9a48-9a0eb0194db1

EID:

2-s2.0-85161470218

Part of ISBN: 9783031308192
Contributors: Leonardo Lima; Andrei Herasimau; Martin Raszyk; Dmitriy Traytel; Simon Yuan
Source: check_circle
University of Copenhagen

Differential Testing of Pushdown Reachability with a Formally Verified Oracle

Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022
2022 | Conference paper | Author
DOI: 10.34727/2022/isbn.978-3-85448-053-2-44
SOURCE-WORK-ID:

dfd28a20-c8a9-4bcc-a5b3-7546f23820d9

EID:

2-s2.0-85148085838

Part of ISBN: 9783854480532
Contributors: Anders Schlichtkrull; Morten Konggaard Schou; Jiří Srba; Dmitriy Traytel
Source: check_circle
University of Copenhagen

Practical Relational Calculus Query Evaluation

25th International Conference on Database Theory (ICDT 2022)
2022 | Conference paper
DOI: 10.4230/LIPICS.ICDT.2022.11
Source: Self-asserted source
Dmitriy Traytel

Verified First-Order Monitoring with Recursive Rules

28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022)
2022 | Conference paper
DOI: 10.1007/978-3-030-99527-0_13
Part of ISBN: 9783030995263
Part of ISBN: 9783030995270
Part of ISSN: 0302-9743
Part of ISSN: 1611-3349
Source: Self-asserted source
Dmitriy Traytel

VeriMon

Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings
2022 | Conference paper | Author
DOI: 10.1007/978-3-031-17715-6_1
SOURCE-WORK-ID:

c9d1d1a8-e016-4a72-9a07-4914bcc9c003

EID:

2-s2.0-85140762044

Part of ISBN: 9783031177149
Contributors: 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 et al.
Source: check_circle
University of Copenhagen

Quotients of Bounded Natural Functors

Logical Methods in Computer Science
2022-02-01 | Journal article
DOI: 10.46298/lmcs-18(1:23)2022
Part of ISSN: 1860-5974
Source: Self-asserted source
Dmitriy Traytel

Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant

Journal of Automated Reasoning
2021 | Journal article | Author
DOI: 10.1007/s10817-021-09599-8
SOURCE-WORK-ID:

5ff9e45b-a74f-4ae4-a890-4ae97b39958d

EID:

2-s2.0-85113754331
Contributors: Andrei Popescu; Dmitriy Traytel
Source: check_circle
University of Copenhagen

Verified Progress Tracking for Timely Dataflow.

12th International Conference on Interactive Theorem Proving (ITP 2021)
2021 | Conference paper | Author
DOI: 10.4230/LIPICS.ITP.2021.10
SOURCE-WORK-ID:

01041a18-6e38-4feb-ac9e-5c17add0c98e

EID:

2-s2.0-85115204531

Part of ISBN: {978-3-95977-188-7
Contributors: Matthias Brun; Sára Decova; Andrea Lattuada; Dmitriy Traytel
Source: check_circle
University of Copenhagen

Scalable online first-order monitoring

International Journal on Software Tools for Technology Transfer
2021-06-05 | Journal article
DOI: 10.1007/s10009-021-00607-1
Part of ISSN: 1433-2779
Contributors: Joshua Schneider; David Basin; Frederik Brix; Srđan Krstić; Dmitriy Traytel
Source: Self-asserted source
Dmitriy Traytel via Crossref Metadata Search

A taxonomy for classifying runtime verification tools

International Journal on Software Tools for Technology Transfer
2021-05 | Journal article
DOI: 10.1007/s10009-021-00609-z
Part of ISSN: 1433-2779
Contributors: Yliès Falcone; Srđan Krstić; Giles Reger; Dmitriy Traytel
Source: Self-asserted source
Dmitriy Traytel via Crossref Metadata Search

A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2020 | Book
DOI: 10.1007/978-3-030-51074-9_25
EID:

2-s2.0-85088260576

Part of ISBN:

16113349 03029743
Contributors: Basin, D.; Dardinier, T.; Heimes, L.; Krstić, S.; Raszyk, M.; Schneider, J.; Traytel, D.
Source: Self-asserted source
Dmitriy Traytel via Scopus - Elsevier

Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Journal of Automated Reasoning
2020 | Journal article
DOI: 10.1007/s10817-020-09561-0
EID:

2-s2.0-85086643610

Part of ISBN:

15730670 01687433
Contributors: Schlichtkrull, A.; Blanchette, J.; Traytel, D.; Waldmann, U.
Source: Self-asserted source
Dmitriy Traytel via Scopus - Elsevier

Multi-head Monitoring of Metric Dynamic Logic

Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings
2020 | Conference paper | Author
DOI: 10.1007/978-3-030-59152-6_13
SOURCE-WORK-ID:

361418bc-6158-413c-848d-217ed43a4f8b

EID:

2-s2.0-85093863993

Part of ISBN: 9783030591519
Contributors: Martin Raszyk; David Basin; Dmitriy Traytel
Source: check_circle
University of Copenhagen

Quotients of Bounded Natural Functors

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2020 | Book
DOI: 10.1007/978-3-030-51054-1_4
EID:

2-s2.0-85088257606

Part of ISBN:

16113349 03029743
Contributors: Fürer, B.; Lochbihler, A.; Schneider, J.; Traytel, D.
Source: Self-asserted source
Dmitriy Traytel via Scopus - Elsevier

A Formally Verified Abstract Account of Gödel's Incompleteness Theorems

CADE-27
2019 | Conference paper
DOI: 10.1007/978-3-030-29436-6_26
Source: Self-asserted source
Dmitriy Traytel

A Formally Verified Monitor for Metric First-Order Temporal Logic

RV 2019
2019 | Conference paper
DOI: 10.1007/978-3-030-32079-9_18
Source: Self-asserted source
Dmitriy Traytel

A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)

Form.\ Methods Syst.\ Des.
2019 | Journal article
DOI: 10.1007/s10703-019-00337-w
Source: Self-asserted source
Dmitriy Traytel

A verified prover based on ordered resolution

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2019
2019 | Conference paper
DOI: 10.1145/3293880.3294100
Part of ISBN: 9781450362221
Contributors: Anders Schlichtkrull; Jasmin Christian Blanchette; Dmitriy Traytel
Source: Self-asserted source
Dmitriy Traytel via Crossref Metadata Search

Adaptive Online First-Order Monitoring

ATVA 2019
2019 | Conference paper
DOI: 10.1007/978-3-030-31784-3_8
SOURCE-WORK-ID:

c5bd004f-40c1-42bd-9984-e68eaead1965

EID:

2-s2.0-85076099490

Part of ISBN:

16113349 03029743
Source: Self-asserted source
Dmitriy Traytel

Almost event-rate independent monitoring

Formal Methods in System Design
2019 | Journal article
DOI: 10.1007/s10703-018-00328-3
EID:

2-s2.0-85061195974

Part of ISBN:

15728102 09259856
Contributors: Basin, D.; Bhatt, B.N.; Krstić, S.; Traytel, D.
Source: Self-asserted source
Dmitriy Traytel via Scopus - Elsevier
grade
Preferred source (of 2)‎

From Nondeterministic to Multi-Head Deterministic Finite-State Transducers

Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany
2019 | Journal article
DOI: 10.4230/LIPICS.ICALP.2019.127
Source: Self-asserted source
Dmitriy Traytel

Generic Authenticated Data Structures, Formally

ITP 2019
2019 | Conference paper
DOI: 10.4230/LIPIcs.ITP.2019.10
DOI: 10.4230/LIPIcs.ITP.2019.14
SOURCE-WORK-ID:

e820378e-56ea-454d-915c-510265cd0db2

EID:

2-s2.0-85074593569

Part of ISBN:

18688969
Source: Self-asserted source
Dmitriy Traytel

Multi-Head Monitoring of Metric Temporal Logic

ATVA 2019
2019 | Conference paper
DOI: 10.1007/978-3-030-31784-3_9
SOURCE-WORK-ID:

353f07a7-77fc-4d25-b1ba-5bdb234f5b66

EID:

2-s2.0-85076084897

Part of ISBN:

16113349 03029743
Source: Self-asserted source
Dmitriy Traytel

Bindings as bounded natural functors

Proceedings of the ACM on Programming Languages
2019-01-02 | Journal article
DOI: 10.1145/3290335
Part of ISSN: 2475-1421
Contributors: Jasmin Christian Blanchette; Lorenzo Gheri; Andrei Popescu; Dmitriy Traytel
Source: Self-asserted source
Dmitriy Traytel via Crossref Metadata Search

A Taxonomy for Classifying Runtime Verification Tools

Runtime Verification
2018 | Other
DOI: 10.1007/978-3-030-03769-7_14
Part of ISBN: 9783030037680
Part of ISSN: 0302-9743
Contributors: Yliès Falcone; Srđan Krstić; Giles Reger; Dmitriy Traytel
Source: Self-asserted source
Dmitriy Traytel via Crossref Metadata Search

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover

IJCAR 2018
2018 | Conference paper
DOI: 10.1007/978-3-319-94205-6_7
Source: Self-asserted source
Dmitriy Traytel

Optimal Proofs for Linear Temporal Logic on Lasso Words

Automated Technology for Verification and Analysis
2018 | Other
DOI: 10.1007/978-3-030-01090-4_3
Part of ISBN: 9783030010898
Part of ISSN: 0302-9743
Contributors: David Basin; Bhargav Nagaraja Bhatt; Dmitriy Traytel
Source: Self-asserted source
Dmitriy Traytel via Crossref Metadata Search

Scalable Online First-Order Monitoring

Runtime Verification
2018 | Other
DOI: 10.1007/978-3-030-03769-7_20
Part of ISBN: 9783030037680
Part of ISSN: 0302-9743
Contributors: Joshua Schneider; David Basin; Frederik Brix; Srđan Krstić; Dmitriy Traytel
Source: Self-asserted source
Dmitriy Traytel via Crossref Metadata Search

A Report of ARCADE 2017

2017 | Conference paper
DOI: 10.29007/143m
Source: Self-asserted source
Dmitriy Traytel
grade
Preferred source (of 2)‎

AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties

2017 | Conference paper
DOI: 10.29007/bm4c
Source: Self-asserted source
Dmitriy Traytel
grade
Preferred source (of 2)‎

Almost Event-Rate Independent Monitoring of Metric Dynamic Logic

Runtime Verification
2017 | Other
DOI: 10.1007/978-3-319-67531-2_6
Part of ISBN: 9783319675305
Part of ISSN: 0302-9743
Contributors: David Basin; Srđan Krstić; Dmitriy Traytel
Source: Self-asserted source
Dmitriy Traytel via Crossref Metadata Search

Almost event-rate independent monitoring of metric temporal logic

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2017 | Book
DOI: 10.1007/978-3-662-54580-5_6
EID:

2-s2.0-85017502907
Contributors: Basin, D.; Bhatt, B.N.; Traytel, D.
Source: Self-asserted source
Dmitriy Traytel via Scopus - Elsevier

Formal Languages, Formally and Coinductively

Logical Methods in Computer Science
2017 | Journal article
DOI: 10.23638/LMCS-13(3:28)2017
Source: Self-asserted source
Dmitriy Traytel

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

FroCoS 2017
2017 | Conference paper
DOI: 10.1007/978-3-319-66167-4_1
Source: Self-asserted source
Dmitriy Traytel
grade
Preferred source (of 2)‎

Foundational nonuniform (Co)datatypes for higher-order logic

32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017
2017 | Conference paper
DOI: 10.1109/LICS.2017.8005071
Source: Self-asserted source
Dmitriy Traytel
grade
Preferred source (of 2)‎

Friends with benefits: Implementing corecursion in foundational proof assistants

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2017 | Book
DOI: 10.1007/978-3-662-54434-1_5
EID:

2-s2.0-85018662884
Contributors: Blanchette, J.C.; Bouzy, A.; Lochbihler, A.; Popescu, A.; Traytel, D.
Source: Self-asserted source
Dmitriy Traytel via Scopus - Elsevier
grade
Preferred source (of 3)‎

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL

2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK
2017 | Conference paper
DOI: 10.4230/LIPIcs.FSCD.2017.11
Source: Self-asserted source
Dmitriy Traytel

Soundness and Completeness Proofs by Coinductive Methods

J. Autom. Reasoning
2017 | Journal article
DOI: 10.1007/s10817-016-9391-3
Source: Self-asserted source
Dmitriy Traytel
grade
Preferred source (of 2)‎

Formal Languages, Formally and Coinductively

1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal
2016 | Conference paper
DOI: 10.4230/LIPIcs.FSCD.2016.31
Source: Self-asserted source
Dmitriy Traytel
grade
Preferred source (of 2)‎

A Coalgebraic Decision Procedure for WS1S

24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany
2015 | Conference paper
DOI: 10.4230/LIPIcs.CSL.2015.487
Source: Self-asserted source
Dmitriy Traytel
grade
Preferred source (of 2)‎

A formalized hierarchy of probabilistic system types: Proof pearl

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2015 | Book
DOI: 10.1007/978-3-319-22102-1_13
EID:

2-s2.0-84944676084
Contributors: Hölzl, J.; Lochbihler, A.; Traytel, D.
Source: Self-asserted source
Dmitriy Traytel via Scopus - Elsevier

Formalizing Symbolic Decision Procedures for Regular Languages

2015 | Dissertation or Thesis
SOURCE-WORK-ID:

038b9082-b81a-40bd-be67-71034a964cc6

URI:

http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20151016-1273011-1-9
Source: Self-asserted source
Dmitriy Traytel
grade
Preferred source (of 2)‎

Foundational extensible corecursion: a proof assistant perspective

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015
2015 | Conference paper
DOI: 10.1145/2784731.2784732
Source: Self-asserted source
Dmitriy Traytel
grade
Preferred source (of 2)‎

Verified decision procedures for MSO on words based on derivatives of regular expressions

J. Funct. Program.
2015 | Journal article
DOI: 10.1017/S0956796815000246
Source: Self-asserted source
Dmitriy Traytel
grade
Preferred source (of 2)‎
Items per page:
Page 1 of 2
How many people are using ORCID?