default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDDmitriy Traytel
Dmytro Traytel
Person information
- affiliation: University of Copenhagen, Denmark
- affiliation: ETH Zürich
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j40]Andrei Herasimau, Jonathan Julián Huerta y Munive, Leonardo Lima, Martin Raszyk, Dmitriy Traytel:
A Verified Proof Checker for Metric First-Order Temporal Logic. Arch. Formal Proofs 2024 (2024)- [c44]François Hublet, Leonardo Lima, David A. Basin, Srdan Krstic, Dmitriy Traytel:
Proactive Real-Time First-Order Enforcement. CAV (2) 2024: 156-181 - [c43]Leonardo Lima
, Jonathan Julián Huerta y Munive, Dmitriy Traytel:
Explainable Online Monitoring of Metric First-Order Temporal Logic. TACAS (1) 2024: 288-307 - [e3]Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy:
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024. ACM 2024 [contents] - [d3]François Hublet, Leonardo Lima, David A. Basin, Srdan Krstic, Dmitriy Traytel:
Artifact for "Proactive Real-Time First-Order Enforcement". Version 3. Zenodo, 2024 [all versions]
- [d2]François Hublet, Leonardo Lima, David A. Basin, Dmitriy Traytel, Srdan Krstic:
Artifact for "Proactive Real-Time First-Order Enforcement". Version 1. Zenodo, 2024 [all versions] - [d1]François Hublet, Leonardo Lima, David A. Basin, Dmitriy Traytel, Srdan Krstic:
Artifact for "Proactive Real-Time First-Order Enforcement". Version 2. Zenodo, 2024 [all versions] - 2023
- [j39]Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel:
Labeled Transition Systems. Arch. Formal Proofs 2023 (2023) - [j38]Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel:
Pushdown Systems. Arch. Formal Proofs 2023 (2023) - [j37]Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel:
Efficient Evaluation of Arbitrary Relational Calculus Queries. Log. Methods Comput. Sci. 19(4) (2023) - [j36]Andrei Popescu, Dmitriy Traytel:
Admissible Types-to-PERs Relativization in Higher-Order Logic. Proc. ACM Program. Lang. 7(POPL): 1214-1245 (2023) - [c42]David A. Basin, Srdan Krstic, Joshua Schneider, Dmitriy Traytel:
Correct and Efficient Policy Monitoring, a Retrospective. ATVA (1) 2023: 3-30 - [c41]Leonardo Lima, Andrei Herasimau, Martin Raszyk, Dmitriy Traytel, Simon Yuan:
Explainable Online Monitoring of Metric Temporal Logic. TACAS (2) 2023: 473-491 - [e2]Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic:
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. ACM 2023 [contents] - 2022
- [j35]Martin Raszyk, Dmitriy Traytel:
Making Arbitrary Relational Calculus Queries Safe-Range. Arch. Formal Proofs 2022 (2022) - [j34]Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel:
Quotients of Bounded Natural Functors. Log. Methods Comput. Sci. 18(1) (2022) - [c40]Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel:
Differential Testing of Pushdown Reachability with a Formally Verified Oracle. FMCAD 2022: 369-379 - [c39]Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel:
Practical Relational Calculus Query Evaluation. ICDT 2022: 11:1-11:21 - [c38]David A. Basin, Thibault Dardinier, Nico Hauser, Lukas Heimes, Jonathan Julián Huerta y Munive, Nicolas Kaletsch, Srdan Krstic, Emanuele Marsicano, Martin Raszyk, Joshua Schneider, Dawit Legesse Tirore, Dmitriy Traytel, Sheila Zingg:
VeriMon: A Formally Verified Monitoring Tool. ICTAC 2022: 1-6 - [c37]Sheila Zingg, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel:
Verified First-Order Monitoring with Recursive Rules. TACAS (2) 2022: 236-253 - [i5]Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel:
Efficient Evaluation of Arbitrary Relational Calculus Queries. CoRR abs/2210.09964 (2022) - 2021
- [j33]Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel:
Formalization of Timely Dataflow's Progress Tracking Protocol. Arch. Formal Proofs 2021 (2021) - [j32]Andrei Popescu, Dmitriy Traytel:
Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant. J. Autom. Reason. 65(7): 1027-1070 (2021) - [j31]Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel:
Scalable online first-order monitoring. Int. J. Softw. Tools Technol. Transf. 23(2): 185-208 (2021) - [j30]Yliès Falcone, Srdan Krstic, Giles Reger, Dmitriy Traytel:
A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf. 23(2): 255-284 (2021) - [c36]Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel:
Verified Progress Tracking for Timely Dataflow. ITP 2021: 10:1-10:20 - [i4]Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel:
Quotients of Bounded Natural Functors. CoRR abs/2104.05348 (2021) - 2020
- [j29]Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider, Dmitriy Traytel:
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations. Arch. Formal Proofs 2020 (2020) - [j28]Ben Fiedler, Dmitriy Traytel:
A Formal Proof of The Chandy-Lamport Distributed Snapshot Algorithm. Arch. Formal Proofs 2020 (2020) - [j27]Lukas Heimes, Dmitriy Traytel, Joshua Schneider:
Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows. Arch. Formal Proofs 2020 (2020) - [j26]Andrei Popescu, Dmitriy Traytel:
From Abstract to Concrete Gödel's Incompleteness Theorems - Part I. Arch. Formal Proofs 2020 (2020) - [j25]Andrei Popescu, Dmitriy Traytel:
From Abstract to Concrete Gödel's Incompleteness Theorems - Part II. Arch. Formal Proofs 2020 (2020) - [j24]Andrei Popescu, Dmitriy Traytel:
An Abstract Formalization of Gödel's Incompleteness Theorems. Arch. Formal Proofs 2020 (2020) - [j23]Andrei Popescu, Dmitriy Traytel:
Robinson Arithmetic. Arch. Formal Proofs 2020 (2020) - [j22]Andrei Popescu, Dmitriy Traytel:
Syntax-Independent Logic Infrastructure. Arch. Formal Proofs 2020 (2020) - [j21]Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. J. Autom. Reason. 64(7): 1169-1195 (2020) - [c35]Martin Raszyk, David A. Basin, Dmitriy Traytel:
Multi-head Monitoring of Metric Dynamic Logic. ATVA 2020: 233-250 - [c34]Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel:
Quotients of Bounded Natural Functors. IJCAR (2) 2020: 58-78 - [c33]David A. Basin, Thibault Dardinier, Lukas Heimes, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel:
A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic. IJCAR (1) 2020: 432-453
2010 – 2019
- 2019
- [j20]Matthias Brun, Dmitriy Traytel:
Formalization of Generic Authenticated Data Structures. Arch. Formal Proofs 2019 (2019) - [j19]Joshua Schneider, Dmitriy Traytel:
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic. Arch. Formal Proofs 2019 (2019) - [j18]César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Yliès Falcone, Adrian Francalanza, Srdan Krstic, João M. Lourenço, Dejan Nickovic, Gordon J. Pace, José Rufino, Julien Signoles, Dmitriy Traytel, Alexander Weiss:
A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des. 54(3): 279-335 (2019) - [j17]David A. Basin, Bhargav Nagaraja Bhatt, Srdan Krstic, Dmitriy Traytel:
Almost event-rate independent monitoring. Formal Methods Syst. Des. 54(3): 449-478 (2019) - [j16]César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Yliès Falcone, Adrian Francalanza, Srdan Krstic, João M. Lourenço, Dejan Nickovic, Gordon J. Pace, José Rufino, Julien Signoles, Dmitriy Traytel, Alexander Weiss:
Correction to: A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des. 55(1): 72 (2019) - [j15]Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel:
Bindings as bounded natural functors. Proc. ACM Program. Lang. 3(POPL): 22:1-22:34 (2019) - [c32]Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel:
Adaptive Online First-Order Monitoring. ATVA 2019: 133-150 - [c31]Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel:
Multi-head Monitoring of Metric Temporal Logic. ATVA 2019: 151-170 - [c30]Andrei Popescu, Dmitriy Traytel:
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. CADE 2019: 442-461 - [c29]Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel:
A verified prover based on ordered resolution. CPP 2019: 152-165 - [c28]Martin Raszyk, David A. Basin, Dmitriy Traytel:
From Nondeterministic to Multi-Head Deterministic Finite-State Transducers. ICALP 2019: 127:1-127:14 - [c27]Matthias Brun, Dmitriy Traytel:
Generic Authenticated Data Structures, Formally. ITP 2019: 10:1-10:18 - [c26]Joshua Schneider, David A. Basin, Srdan Krstic, Dmitriy Traytel:
A Formally Verified Monitor for Metric First-Order Temporal Logic. RV 2019: 310-328 - 2018
- [j14]Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018) - [j13]Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel:
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018) - [c25]David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel:
Optimal Proofs for Linear Temporal Logic on Lasso Words. ATVA 2018: 37-55 - [c24]Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. IJCAR 2018: 89-107 - [c23]Yliès Falcone, Srdan Krstic, Giles Reger, Dmitriy Traytel:
A Taxonomy for Classifying Runtime Verification Tools. RV 2018: 241-262 - [c22]Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel:
Scalable Online First-Order Monitoring. RV 2018: 353-371 - [i3]César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Yliès Falcone, Adrian Francalanza, Srdan Krstic, João M. Lourenço, Dejan Nickovic, Gordon J. Pace, José Rufino, Julien Signoles, Dmitriy Traytel, Alexander Weiss:
A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software). CoRR abs/1811.06740 (2018) - 2017
- [j12]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Abstract Soundness. Arch. Formal Proofs 2017 (2017) - [j11]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Operations on Bounded Natural Functors. Arch. Formal Proofs 2017 (2017) - [j10]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Soundness and Completeness Proofs by Coinductive Methods. J. Autom. Reason. 58(1): 149-179 (2017) - [j9]Dmitriy Traytel:
Formal Languages, Formally and Coinductively. Log. Methods Comput. Sci. 13(3) (2017) - [c21]Giles Reger, Dmitriy Traytel:
A Report of ARCADE 2017. ARCADE@CADE 2017: 1-5 - [c20]Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel:
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP 2017: 111-140 - [c19]Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel:
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS 2017: 3-21 - [c18]Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel:
Foundational nonuniform (Co)datatypes for higher-order logic. LICS 2017: 1-12 - [c17]Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel:
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. FSCD 2017: 11:1-11:18 - [c16]David A. Basin, Srdjan Krstic, Dmitriy Traytel:
AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties. RV-CuBES 2017: 29-36 - [c15]David A. Basin, Srdan Krstic, Dmitriy Traytel:
Almost Event-Rate Independent Monitoring of Metric Dynamic Logic. RV 2017: 85-102 - [c14]David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel:
Almost Event-Rate Independent Monitoring of Metric Temporal Logic. TACAS (2) 2017: 94-112 - [e1]Giles Reger, Dmitriy Traytel:
ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017. EPiC Series in Computing 51, EasyChair 2017 [contents] - 2016
- [j8]Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel:
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. Arch. Formal Proofs 2016 (2016) - [c13]Dmitriy Traytel:
Formal Languages, Formally and Coinductively. FSCD 2016: 31:1-31:17 - [i2]Dmitriy Traytel:
Formal Languages, Formally and Coinductively. CoRR abs/1611.09633 (2016) - 2015
- [b1]Dmytro Traytel:
Formalizing Symbolic Decision Procedures for Regular Languages. Technical University Munich, 2015 - [j7]Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel:
A Zoo of Probabilistic Systems. Arch. Formal Proofs 2015 (2015) - [j6]Dmitriy Traytel:
Derivatives of Logical Formulas. Arch. Formal Proofs 2015 (2015) - [j5]Dmitriy Traytel, Tobias Nipkow:
Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. 25 (2015) - [c12]Dmitriy Traytel:
A Coalgebraic Decision Procedure for WS1S. CSL 2015: 487-503 - [c11]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Witnessing (Co)datatypes. ESOP 2015: 359-382 - [c10]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Foundational extensible corecursion: a proof assistant perspective. ICFP 2015: 192-204 - [c9]Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel:
A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. ITP 2015: 203-220 - [i1]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Foundational Extensible Corecursion. CoRR abs/1501.05425 (2015) - 2014
- [j4]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Abstract Completeness. Arch. Formal Proofs 2014 (2014) - [j3]Tobias Nipkow, Dmitriy Traytel:
Unified Decision Procedures for Regular Expression Equivalence. Arch. Formal Proofs 2014 (2014) - [j2]Dmitriy Traytel, Tobias Nipkow:
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions. Arch. Formal Proofs 2014 (2014) - [c8]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Unified Classical Logic Completeness - A Coinductive Pearl. IJCAR 2014: 46-60 - [c7]Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel:
Experience report: the next 1100 Haskell programmers. Haskell 2014: 25-30 - [c6]Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel:
Truly Modular (Co)datatypes for Isabelle/HOL. ITP 2014: 93-110 - [c5]Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Cardinals in Isabelle/HOL. ITP 2014: 111-127 - [c4]Tobias Nipkow, Dmitriy Traytel:
Unified Decision Procedures for Regular Expression Equivalence. ITP 2014: 450-466 - 2013
- [j1]Dmitriy Traytel:
A Codatatype of Formal Languages. Arch. Formal Proofs 2013 (2013) - [c3]Dmitriy Traytel, Tobias Nipkow:
Verified decision procedures for MSO on words based on derivatives of regular expressions. ICFP 2013: 3-12 - 2012
- [c2]Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette:
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. LICS 2012: 596-605 - 2011
- [c1]Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow:
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. APLAS 2011: 89-104
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-17 23:37 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
