Dmitriy Traytel
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
46
Venues
17
Active years
2011–2025
Best venue rank
A*
Where they publish
Papers
46 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | CAV | Scaling Up Proactive Enforcement. | Franois Hublet, Leonardo Lima, David A. Basin, Srdan Krstic, Dmitriy Traytel |
| 2025 | ITP | Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. | Jan van Brgge, Andrei Popescu, Dmitriy Traytel |
| 2025 | ITP | Nondeterministic Asynchronous Dataflow in Isabelle/HOL. | Rafael Castro Gonalves Silva, Laouen Fernet, Dmitriy Traytel |
| 2024 | ATVA | WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts. | Leonardo Lima, Jonathan Julin Huerta y Munive, Dmitriy Traytel |
| 2024 | CAV | Proactive Real-Time First-Order Enforcement. | Franois Hublet, Leonardo Lima, David A. Basin, Srdan Krstic, Dmitriy Traytel |
| 2024 | RV | TimelyMon: A Streaming Parallel First-Order Monitor. | Lennard Reese, Rafael Castro Gonalves Silva, Dmitriy Traytel |
| 2024 | TACAS | Explainable Online Monitoring of Metric First-Order Temporal Logic. | Leonardo Lima, Jonathan Julin Huerta y Munive, Dmitriy Traytel |
| 2023 | ATVA | Correct and Efficient Policy Monitoring, a Retrospective. | David A. Basin, Srdan Krstic, Joshua Schneider, Dmitriy Traytel |
| 2023 | TACAS | Explainable Online Monitoring of Metric Temporal Logic. | Leonardo Lima, Andrei Herasimau, Martin Raszyk, Dmitriy Traytel, Simon Yuan |
| 2022 | FMCAD | Differential Testing of Pushdown Reachability with a Formally Verified Oracle. | Anders Schlichtkrull, Morten Konggaard Schou, Jir Srba, Dmitriy Traytel |
| 2022 | ICDT | Practical Relational Calculus Query Evaluation. | Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel |
| 2022 | ICTAC | VeriMon: A Formally Verified Monitoring Tool. | David A. Basin, Thibault Dardinier, Nico Hauser, Lukas Heimes, Jonathan Julin Huerta y Munive, Nicolas Kaletsch, Srdan Krstic, Emanuele Marsicano, Martin Raszyk, Joshua Schneider, Dawit Legesse Tirore, Dmitriy Traytel, Sheila Zingg |
| 2022 | TACAS | Verified First-Order Monitoring with Recursive Rules. | Sheila Zingg, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel |
| 2021 | ITP | Verified Progress Tracking for Timely Dataflow. | Matthias Brun, Sra Decova, Andrea Lattuada, Dmitriy Traytel |
| 2020 | ATVA | Multi-head Monitoring of Metric Dynamic Logic. | Martin Raszyk, David A. Basin, Dmitriy Traytel |
| 2020 | CADE | A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic. | David A. Basin, Thibault Dardinier, Lukas Heimes, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel |
| 2020 | CADE | Quotients of Bounded Natural Functors. | Basil Frer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel |
| 2019 | ATVA | Adaptive Online First-Order Monitoring. | Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel |
| 2019 | ATVA | Multi-head Monitoring of Metric Temporal Logic. | Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel |
| 2019 | CADE | A Formally Verified Abstract Account of Gdel's Incompleteness Theorems. | Andrei Popescu, Dmitriy Traytel |
| 2019 | CPP | A verified prover based on ordered resolution. | Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel |
| 2019 | ICALP | From Nondeterministic to Multi-Head Deterministic Finite-State Transducers. | Martin Raszyk, David A. Basin, Dmitriy Traytel |
| 2019 | ITP | Generic Authenticated Data Structures, Formally. | Matthias Brun, Dmitriy Traytel |
| 2019 | RV | A Formally Verified Monitor for Metric First-Order Temporal Logic. | Joshua Schneider, David A. Basin, Srdan Krstic, Dmitriy Traytel |
| 2018 | ATVA | Optimal Proofs for Linear Temporal Logic on Lasso Words. | David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel |
| 2018 | CADE | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. | Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann |
| 2018 | RV | A Taxonomy for Classifying Runtime Verification Tools. | Ylis Falcone, Srdan Krstic, Giles Reger, Dmitriy Traytel |
| 2018 | RV | Scalable Online First-Order Monitoring. | Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel |
| 2017 | CADE | A Report of ARCADE 2017. | Giles Reger, Dmitriy Traytel |
| 2017 | ESOP | Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. | Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel |
| 2017 | LICS | Foundational nonuniform (Co)datatypes for higher-order logic. | Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel |
| 2017 | RV | Almost Event-Rate Independent Monitoring of Metric Dynamic Logic. | David A. Basin, Srdan Krstic, Dmitriy Traytel |
| 2017 | RV | AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties. | David A. Basin, Srdjan Krstic, Dmitriy Traytel |
| 2017 | TACAS | Almost Event-Rate Independent Monitoring of Metric Temporal Logic. | David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel |
| 2015 | CSL | A Coalgebraic Decision Procedure for WS1S. | Dmitriy Traytel |
| 2015 | ESOP | Witnessing (Co)datatypes. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2015 | ICFP | Foundational extensible corecursion: a proof assistant perspective. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2015 | ITP | A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. | Johannes Hlzl, Andreas Lochbihler, Dmitriy Traytel |
| 2014 | CADE | Unified Classical Logic Completeness - A Coinductive Pearl. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2014 | HASKELL | Experience report: the next 1100 Haskell programmers. | Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel |
| 2014 | ITP | Cardinals in Isabelle/HOL. | Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel |
| 2014 | ITP | Truly Modular (Co)datatypes for Isabelle/HOL. | Jasmin Christian Blanchette, Johannes Hlzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel |
| 2014 | ITP | Unified Decision Procedures for Regular Expression Equivalence. | Tobias Nipkow, Dmitriy Traytel |
| 2013 | ICFP | Verified decision procedures for MSO on words based on derivatives of regular expressions. | Dmitriy Traytel, Tobias Nipkow |
| 2012 | LICS | Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. | Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette |
| 2011 | APLAS | Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. | Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow |