Dmitriy Traytel

Dmitriy Traytel

Associate Professor - Promotion Programme


  1. 2017
  2. 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 proceedingArticle in proceedingsResearchpeer-review

  3. 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 proceedingArticle in proceedingsResearchpeer-review

  4. 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 journalJournal articleResearchpeer-review

  5. 2018
  6. 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 proceedingArticle in proceedingsResearchpeer-review

  7. 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 proceedingArticle in proceedingsResearchpeer-review

  8. 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 proceedingArticle in proceedingsResearchpeer-review

  9. 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 proceedingArticle in proceedingsResearchpeer-review

  10. 2019
  11. 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 proceedingArticle in proceedingsResearchpeer-review

  12. 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 proceedingArticle in proceedingsResearchpeer-review

  13. 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 journalJournal articleResearchpeer-review

ID: 245399103