Dmitriy Traytel

Publication Activity (10 Years)

Years Active: 2011-2024
Publications (10 Years): 77

Top Topics

Formal Languages

Application Domains

Top Venues

Arch. Formal Proofs

Publications

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)
François Hublet, Leonardo Lima, David A. Basin, Srdan Krstic, Dmitriy Traytel
Proactive Real-Time First-Order Enforcement. CAV (2) (2024)
Leonardo Lima, Jonathan Julián Huerta y Munive, Dmitriy Traytel
Explainable Online Monitoring of Metric First-Order Temporal Logic. TACAS (1) (2024)
Andrei Popescu, Dmitriy Traytel
Admissible Types-to-PERs Relativization in Higher-Order Logic. Proc. ACM Program. Lang. 7 (POPL) (2023)
Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel
Labeled Transition Systems. Arch. Formal Proofs 2023 (2023)
Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel
Efficient Evaluation of Arbitrary Relational Calculus Queries. Log. Methods Comput. Sci. 19 (4) (2023)
Leonardo Lima, Andrei Herasimau, Martin Raszyk, Dmitriy Traytel, Simon Yuan
Explainable Online Monitoring of Metric Temporal Logic. TACAS (2) (2023)
David A. Basin, Srdan Krstic, Joshua Schneider, Dmitriy Traytel
Correct and Efficient Policy Monitoring, a Retrospective. ATVA (1) (2023)
Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel
Pushdown Systems. Arch. Formal Proofs 2023 (2023)
Martin Raszyk, Dmitriy Traytel
Making Arbitrary Relational Calculus Queries Safe-Range. Arch. Formal Proofs 2022 (2022)
Sheila Zingg, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
Verified First-Order Monitoring with Recursive Rules. TACAS (2) (2022)
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)
Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel
Differential Testing of Pushdown Reachability with a Formally Verified Oracle. FMCAD (2022)
Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel
Practical Relational Calculus Query Evaluation. ICDT (2022)
Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
Quotients of Bounded Natural Functors. Log. Methods Comput. Sci. 18 (1) (2022)
Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel
Efficient Evaluation of Arbitrary Relational Calculus Queries. CoRR (2022)
Yliès Falcone, Srdan Krstic, Giles Reger, Dmitriy Traytel
A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf. 23 (2) (2021)
Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel
Verified Progress Tracking for Timely Dataflow. ITP (2021)
Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
Quotients of Bounded Natural Functors. CoRR (2021)
Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel
Scalable online first-order monitoring. Int. J. Softw. Tools Technol. Transf. 23 (2) (2021)
Andrei Popescu, Dmitriy Traytel
Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant. J. Autom. Reason. 65 (7) (2021)
Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel
Formalization of Timely Dataflow's Progress Tracking Protocol. Arch. Formal Proofs 2021 (2021)
Andrei Popescu, Dmitriy Traytel
Robinson Arithmetic. Arch. Formal Proofs 2020 (2020)
Andrei Popescu, Dmitriy Traytel
From Abstract to Concrete Gödel's Incompleteness Theorems - Part I. Arch. Formal Proofs 2020 (2020)
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)
Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
Quotients of Bounded Natural Functors. IJCAR (2) (2020)
Ben Fiedler, Dmitriy Traytel
A Formal Proof of The Chandy-Lamport Distributed Snapshot Algorithm. Arch. Formal Proofs 2020 (2020)
Lukas Heimes, Dmitriy Traytel, Joshua Schneider
Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows. Arch. Formal Proofs 2020 (2020)
Andrei Popescu, Dmitriy Traytel
Syntax-Independent Logic Infrastructure. Arch. Formal Proofs 2020 (2020)
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)
Martin Raszyk, David A. Basin, Dmitriy Traytel
Multi-head Monitoring of Metric Dynamic Logic. ATVA (2020)
Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. J. Autom. Reason. 64 (7) (2020)
Andrei Popescu, Dmitriy Traytel
An Abstract Formalization of Gödel's Incompleteness Theorems. Arch. Formal Proofs 2020 (2020)
Andrei Popescu, Dmitriy Traytel
From Abstract to Concrete Gödel's Incompleteness Theorems - Part II. Arch. Formal Proofs 2020 (2020)
Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel
Multi-head Monitoring of Metric Temporal Logic. ATVA (2019)
Joshua Schneider, Dmitriy Traytel
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic. Arch. Formal Proofs 2019 (2019)
Matthias Brun, Dmitriy Traytel
Formalization of Generic Authenticated Data Structures. Arch. Formal Proofs 2019 (2019)
Matthias Brun, Dmitriy Traytel
Generic Authenticated Data Structures, Formally. ITP (2019)
David A. Basin, Bhargav Nagaraja Bhatt, Srdan Krstic, Dmitriy Traytel
Almost event-rate independent monitoring. Formal Methods Syst. Des. 54 (3) (2019)
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
Bindings as bounded natural functors. Proc. ACM Program. Lang. 3 (POPL) (2019)
Martin Raszyk, David A. Basin, Dmitriy Traytel
From Nondeterministic to Multi-Head Deterministic Finite-State Transducers. ICALP (2019)
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) (2019)
Joshua Schneider, David A. Basin, Srdan Krstic, Dmitriy Traytel
A Formally Verified Monitor for Metric First-Order Temporal Logic. RV (2019)
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) (2019)
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel
A verified prover based on ordered resolution. CPP (2019)
Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel
Adaptive Online First-Order Monitoring. ATVA (2019)
Andrei Popescu, Dmitriy Traytel
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. CADE (2019)
David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel
Optimal Proofs for Linear Temporal Logic on Lasso Words. ATVA (2018)
Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel
Scalable Online First-Order Monitoring. RV (2018)
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018)
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 (2018)
Yliès Falcone, Srdan Krstic, Giles Reger, Dmitriy Traytel
A Taxonomy for Classifying Runtime Verification Tools. RV (2018)
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. IJCAR (2018)
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018)
Giles Reger, Dmitriy Traytel
A Report of ARCADE 2017. ARCADE@CADE (2017)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Abstract Soundness. Arch. Formal Proofs 2017 (2017)
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP (2017)
David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel
Almost Event-Rate Independent Monitoring of Metric Temporal Logic. TACAS (2) (2017)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Soundness and Completeness Proofs by Coinductive Methods. J. Autom. Reason. 58 (1) (2017)
David A. Basin, Srdan Krstic, Dmitriy Traytel
Almost Event-Rate Independent Monitoring of Metric Dynamic Logic. RV (2017)
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)
Dmitriy Traytel
Formal Languages, Formally and Coinductively. Log. Methods Comput. Sci. 13 (3) (2017)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Operations on Bounded Natural Functors. Arch. Formal Proofs 2017 (2017)
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. FSCD (2017)
David A. Basin, Srdjan Krstic, Dmitriy Traytel
AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties. RV-CuBES (2017)
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel
Foundational nonuniform (Co)datatypes for higher-order logic. LICS (2017)
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. Arch. Formal Proofs 2016 (2016)
Dmitriy Traytel
Formal Languages, Formally and Coinductively. CoRR (2016)
Dmitriy Traytel
Formal Languages, Formally and Coinductively. FSCD (2016)
Dmitriy Traytel, Tobias Nipkow
Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. 25 (2015)
Dmitriy Traytel
Derivatives of Logical Formulas. Arch. Formal Proofs 2015 (2015)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Foundational extensible corecursion: a proof assistant perspective. ICFP (2015)
Dmitriy Traytel
A Coalgebraic Decision Procedure for WS1S. CSL (2015)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Foundational Extensible Corecursion. CoRR (2015)
Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel
A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. ITP (2015)
Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel
A Zoo of Probabilistic Systems. Arch. Formal Proofs 2015 (2015)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Witnessing (Co)datatypes. ESOP (2015)
Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel
Truly Modular (Co)datatypes for Isabelle/HOL. ITP (2014)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Cardinals in Isabelle/HOL. ITP (2014)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Abstract Completeness. Arch. Formal Proofs 2014 (2014)
Tobias Nipkow, Dmitriy Traytel
Unified Decision Procedures for Regular Expression Equivalence. ITP (2014)
Tobias Nipkow, Dmitriy Traytel
Unified Decision Procedures for Regular Expression Equivalence. Arch. Formal Proofs 2014 (2014)
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Unified Classical Logic Completeness - A Coinductive Pearl. IJCAR (2014)
Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel
Experience report: the next 1100 Haskell programmers. Haskell (2014)
Dmitriy Traytel, Tobias Nipkow
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions. Arch. Formal Proofs 2014 (2014)
Dmitriy Traytel, Tobias Nipkow
Verified decision procedures for MSO on words based on derivatives of regular expressions. ICFP (2013)
Dmitriy Traytel
A Codatatype of Formal Languages. Arch. Formal Proofs 2013 (2013)
Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. LICS (2012)
Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. APLAS (2011)