Dmitriy Traytel
Associate Professor - Promotion Programme
Software, Data, People & Society
Sigurdsgade 41
2200 København N.
- 2023
- Published
Admissible Types-to-PERs Relativization in Higher-Order Logic
Popescu, A. & Traytel, Dmitriy, 2023, In: Proceedings of the ACM on Programming Languages. 7, POPL, 32 p., 42.Research output: Contribution to journal › Journal article › Research › peer-review
- Published
Correct and Efficient Policy Monitoring, a Retrospective
Basin, D., Krstić, S., Schneider, J. & Traytel, Dmitriy, 2023, Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings. André, É. & Sun, J. (eds.). Springer, p. 3-30 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14215 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- Published
Efficient Evaluation of Arbitrary Relational Calculus Queries
Raszyk, M., Basin, D., Krstić, S. & Traytel, Dmitriy, 2023, In: Logical Methods in Computer Science. 19, 4Research output: Contribution to journal › Journal article › Research › peer-review
- Published
Explainable Online Monitoring of Metric Temporal Logic
Lima, Leonardo, Herasimau, A., Raszyk, M., Traytel, Dmitriy & Yuan, S., 2023, 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. Sankaranarayanan, S. & Sharygina, N. (eds.). Springer, p. 473-491 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13994 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2022
- Published
Differential Testing of Pushdown Reachability with a Formally Verified Oracle
Schlichtkrull, A., Schou, M. K., Srba, J. & Traytel, Dmitriy, 2022, Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022. Griggio, A. & Rungta, N. (eds.). TU Wien Academic Press, p. 369-379Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- Published
Practical Relational Calculus Query Evaluation
Raszyk, M., Basin, D., Krstić, S. & Traytel, Dmitriy, 2022, 25th International Conference on Database Theory, ICDT 2022. Olteanu, D. & Vortmeier, N. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, p. 1-21 11. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 220).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- Published
Quotients of Bounded Natural Functors
Fürer, B., Lochbihler, A., Schneider, J. & Traytel, Dmitriy, 2022, In: Logical Methods in Computer Science. 18, 1, p. 1-28 23.Research output: Contribution to journal › Journal article › Research › peer-review
- Published
VeriMon: A Formally Verified Monitoring Tool
Basin, D., Dardinier, T., Hauser, N., Heimes, L., Huerta y Munive, J. J., Kaletsch, N., Krstić, S., Marsicano, E., Raszyk, M., Schneider, J., Tirore, D. L., Traytel, Dmitriy & Zingg, S., 2022, Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. Seidl, H., Liu, Z. & Pasareanu, C. S. (eds.). Springer, p. 1-6 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13572 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- Published
Verified First-Order Monitoring with Recursive Rules
Zingg, S., Krstić, S., Raszyk, M., Schneider, J. & Traytel, Dmitriy, 2022, Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. Fisman, D. & Rosu, G. (eds.). Springer, Vol. 2. p. 236-253 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13244 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2021
- Published
A taxonomy for classifying runtime verification tools.
Falcone, Y., Krstić, S., Reger, G. & Traytel, Dmitriy, 2021, In: International Journal on Software Tools for Technology Transfer. 23, 2, p. 255-284Research output: Contribution to journal › Journal article › Research › peer-review
- Published
Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant
Popescu, A. & Traytel, Dmitriy, 2021, In: Journal of Automated Reasoning. 65, p. 1027–1070Research output: Contribution to journal › Journal article › Research › peer-review
- Published
Scalable online first-order monitoring
Schneider, J., Basin, D., Brix, F., Krstić, S. & Traytel, Dmitriy, 2021, In: International Journal on Software Tools for Technology Transfer. 23, 2, p. 185-208Research output: Contribution to journal › Journal article › Research › peer-review
- Published
Verified Progress Tracking for Timely Dataflow.
Brun, M., Decova, S., Lattuada, A. & Traytel, Dmitriy, 2021, 12th International Conference on Interactive Theorem Proving (ITP 2021). Cohen, L. & Kaliszyk, C. (eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, p. 1-20 10. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 193).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2020
A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Basin, D., Dardinier, T., Heimes, L., Krstić, S., Raszyk, M., Schneider, J. & Traytel, Dmitriy, 2020, IJCAR 2020. Vol. 12166. p. 432-453 22 p. (Lecture Notes in Computer Science, Vol. 12166).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Schlichtkrull, A., Blanchette, J. C., Traytel, Dmitriy & Waldmann, U., 2020, In: Journal of Automated Reasoning. 64, p. 1169–1195Research output: Contribution to journal › Journal article › Research › peer-review
- Published
Multi-head Monitoring of Metric Dynamic Logic
Raszyk, M., Basin, D. & Traytel, Dmitriy, 2020, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. Hung, D. V. & Sokolsky, O. (eds.). Springer, p. 233-250 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 12302 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Quotients of Bounded Natural Functors
Fürer, B., Lochbihler, A., Schneider, J. & Traytel, Dmitriy, 2020, IJCAR 2020. Peltier, N. & Sofronie-Stokkermans, V. (eds.). Springer, Cham, Vol. 12167. p. 58-78 21 p. (Lecture Notes in Computer Science, Vol. 12167).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2019
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
Popescu, A. & Traytel, Dmitriy, 2019, CADE-27. Fontaine, P. (ed.). Springer, Cham, Vol. 11716. p. 442-461 20 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
A Formally Verified Monitor for Metric First-Order Temporal Logic
Schneider, J., Basin, D., Krstić, S. & Traytel, Dmitriy, 2019, RV 2019. Finkbeiner, B. & Mariani, L. (eds.). Springer, Cham, Vol. 11757. p. 310-328 19 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)
Sánchez, C., Schneider, G., Ahrendt, W., Bartocci, E., Bianculli, D., Colombo, C., Falcone, Y., Francalanza, A., Krstić, S., Lourenço, J. M., Nickovic, D., Pace, G. J., Rufino, J., Signoles, J., Traytel, Dmitriy & Weiss, A., 2019, In: Formal Methods in System Design. 54, 3, p. 279-335 57 p.Research output: Contribution to journal › Journal article › Research › peer-review
A Verified Prover Based on Ordered Resolution
Schlichtkrull, A., Blanchette, J. C. & Traytel, Dmitriy, 2019, CPP 2019. Mahboubi, A. & Myreen, M. O. (eds.). ACM, p. 152-165 14 p.Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Adaptive Online First-Order Monitoring
Schneider, J., Basin, D., Brix, F., Krstić, S. & Traytel, Dmitriy, 2019, ATVA 2019. Chen, Y-F., Cheng, C-H. & Esparza, J. (eds.). Springer, Cham, Vol. 11781. p. 133-150 18 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Almost Event-Rate Independent Monitoring
Basin, D., Bhatt, B., Krstić, S. & Traytel, Dmitriy, 2019, In: Formal Methods in System Design. 54, 3, p. 449-478 30 p.Research output: Contribution to journal › Journal article › Research › peer-review
Bindings as Bounded Natural Functors
Blanchette, J. C., Gheri, L., Popescu, A. & Traytel, Dmitriy, 2019, In: Proceedings of the ACM on Programming Languages. 3, POPL, p. 22:1-22:34Research output: Contribution to journal › Journal article › Research › peer-review
From Nondeterministic to Multi-Head Deterministic Finite-State Transducers
Raszyk, M., Basin, D. & Traytel, Dmitriy, 2019, ICALP 2019. Baier, C., Chatzigiannakis, I., Flocchini, P. & Leonardi, S. (eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Vol. 132. p. 127:1-127:14 (LIPIcs).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Generic Authenticated Data Structures, Formally
Brun, M. & Traytel, Dmitriy, 2019, ITP 2019. Harrison, J., O'Leary, J. & Tolmach, A. (eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Vol. 141. p. 10:1-10:18 (LIPIcs).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Multi-Head Monitoring of Metric Temporal Logic
Raszyk, M., Basin, D., Krstić, S. & Traytel, Dmitriy, 2019, ATVA 2019. Chen, Y-F., Cheng, C-H. & Esparza, J. (eds.). Springer, Cham, Vol. 11781. p. 151-170 20 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2018
A Taxonomy for Classifying Runtime Verification Tools
Falcone, Y., Krstić, S., Reger, G. & Traytel, Dmitriy, 2018, Runtime Verification: 18th International Conference, RV 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings. Colombo, C. & Leucker, M. (eds.). Springer, p. 241-262 22 p. (LNCS). (Lecture Notes in Computer Science, Vol. 11237).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Schlichtkrull, A., Blanchette, J. C., Traytel, Dmitriy & Waldmann, U., 2018, IJCAR 2018. Galmiche, D., Schulz, S. & Sebastiani, R. (eds.). Springer, Cham, Vol. 10900. p. 89-107 19 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Optimal Proofs for Linear Temporal Logic on Lasso Words
Basin, D., Bhatt, B. & Traytel, Dmitriy, 2018, Automated Technology for Verification and Analysis: 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Lahiri, S. & Wang, C. (eds.). Springer, p. 37-55 19 p. (LNCS, Vol. 11138).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Scalable Online First-Order Monitoring
Schneider, J., Basin, D., Brix, F., Krstić, S. & Traytel, Dmitriy, 2018, RV 2018. Colombo, C. & Leucker, M. (eds.). Springer, Cham, Vol. 11237. p. 353-371 19 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2017
Almost Event-Rate Independent Monitoring of Metric Dynamic Logic
Basin, D., Krstić, S. & Traytel, Dmitriy, 2017, Runtime Verification: 17th International Conference, RV 2017, Seattle, WA, USA, September 13-16, 2017, Proceedings. Lahiri, S. & Reger, G. (eds.). Springer, Cham, p. 85-102 18 p. (Lecture Notes in Computer Science, Vol. 10548).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
Basin, D., Bhatt, B. & Traytel, Dmitriy, 2017, TACAS 2017. Legay, A. & Margaria, T. (eds.). Springer Berlin/Heidelberg, Vol. 10206. p. 94-112 19 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Formal Languages, Formally and Coinductively
Traytel, Dmitriy, 2017, In: Logical Methods in Computer Science. 13, 3, p. 1-22 28.Research output: Contribution to journal › Journal article › Research › peer-review
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
Biendarra, J., Blanchette, J. C., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kunčar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R. & Traytel, Dmitriy, 2017, FroCoS 2017. Dixon, C. & Finger, M. (eds.). Springer, Cham, Vol. 10483. p. 3-21 19 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Foundational Nonuniform (Co)datatypes for Higher-Order Logic
Blanchette, J. C., Meier, F., Popescu, A. & Traytel, Dmitriy, 2017, LICS 2017. IEEE Computer Society Press, p. 1-12 12 p.Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants
Blanchette, J. C., Bouzy, A., Lochbihler, A., Popescu, A. & Traytel, Dmitriy, 2017, ESOP 2017. Yang, H. (ed.). Springer Berlin/Heidelberg, Vol. 10201. p. 111-140 30 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
Blanchette, J. C., Fleury, M. & Traytel, Dmitriy, 2017, FSCD 2017. Miller, D. (ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Vol. 84. p. 11:1-11:18 (LIPIcs).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Soundness and Completeness Proofs by Coinductive Methods
Blanchette, J. C., Popescu, A. & Traytel, Dmitriy, 2017, In: Journal of Automated Reasoning. 58, 1, p. 149-179 31 p.Research output: Contribution to journal › Journal article › Research › peer-review
- 2016
Formal Languages, Formally and Coinductively
Traytel, Dmitriy, 2016, FSCD 2016. Kesner, D. & Pientka, B. (eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Vol. 52. p. 31:1-31:17 (LIPIcs).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2015
Formalizing Symbolic Decision Procedures for Regular Languages
Traytel, Dmitriy, 15 Oct 2015, Technische Universität München . 132 p.Research output: Book/Report › Doctoral thesis › Research
A Coalgebraic Decision Procedure for WS1S
Traytel, Dmitriy, 2015, CSL 2015. Kreutzer, S. (ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Vol. 41. p. 487-503 17 p. (LIPIcs).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
A Formalized Hierarchy of Probabilistic System Types (Proof Pearl)
Hölzl, J., Lochbihler, A. & Traytel, Dmitriy, 2015, ITP 2015. Zhang, X. & Urban, C. (eds.). Springer, Cham, Vol. 9236. p. 203-220 18 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Foundational Extensible Corecursion
Blanchette, J. C., Popescu, A. & Traytel, Dmitriy, 2015, ICFP 2015. Reppy, J. (ed.). ACM, p. 192-204 13 p.Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Traytel, Dmitriy & Nipkow, T., 2015, In: Journal of Functional Programming. 25Research output: Contribution to journal › Journal article › Research › peer-review
Witnessing (Co)datatypes
Blanchette, J. C., Popescu, A. & Traytel, Dmitriy, 2015, Programming Languages and Systems: 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. Vitek, J. (ed.). Springer, p. 359-382 24 p. (Lecture Notes in Computer Science, Vol. 9032).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2014
Cardinals in Isabelle/HOL
Blanchette, J. C., Popescu, A. & Traytel, Dmitriy, 2014, ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. Klein, G. & Gamboa, R. (eds.). Springer, Cham, p. 111-127 17 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Experience Report: The Next 1100 Haskell Programmers
Blanchette, J. C., Hupel, L., Nipkow, T., Noschinski, L. & Traytel, Dmitriy, 2014, Haskell '14: Proceedings of the 2014 ACM SIGPLAN symposium on Haskell. Swiestra, W. (ed.). ACM, p. 25-30 6 p.Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Truly Modular (Co)datatypes for Isabelle/HOL
Blanchette, J. C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A. & Traytel, Dmitriy, 2014, ITP 2014 - : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. Klein, G. & Gamboa, R. (eds.). Springer, Cham, Vol. 8558. p. 93-110 18 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Unified Classical Logic Completeness - A Coinductive Pearl
Blanchette, J. C., Popescu, A. & Traytel, Dmitriy, 2014, Automated Reasoning: 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Vienna, Austria, July 19-22, 2014, Proceedings. Demri, S., Kapur, D. & Weidenbach, C. (eds.). Springer, Cham, p. 46-60 15 p. (Lecture Notes in Computer Science, Vol. 8562).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Unified Decision Procedures for Regular Expression Equivalence
Nipkow, T. & Traytel, Dmitriy, 2014, ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. Klein, G. & Gamboa, R. (eds.). Springer, Cham, Vol. 8558. p. 450-466 17 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2013
Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Traytel, Dmitriy & Nipkow, T., 2013, ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming. Morrisett, G. & Uustalu, T. (eds.). ACM, p. 3-12 10 p.Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2012
Foundational, Compositional (Co)datatypes for Higher-Order Logic—Category Theory Applied to Theorem Proving
Traytel, Dmitriy, Popescu, A. & Blanchette, J. C., 2012, LICS 2012. IEEE Computer Society Press, p. 596-605 10 p.Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
- 2011
- Published
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping
Traytel, Dmitriy, Berghofer, S. & Nipkow, T., 2011, APLAS 2011. Yang, H. (ed.). Springer Berlin/Heidelberg, Vol. 7078. p. 89-104 16 p. (LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
ID: 245399103
Most downloads
-
16
downloads
Verified Progress Tracking for Timely Dataflow.
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Published -
15
downloads
Practical Relational Calculus Query Evaluation
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Published -
14
downloads
Explainable Online Monitoring of Metric Temporal Logic
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Published