Dmitriy Traytel

According to our database, Dmitriy Traytel authored at least 83 papers between 2011 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Artifact for "Proactive Real-Time First-Order Enforcement".

François Hublet, Leonardo Lima, David A. Basin, Dmitriy Traytel, Srdan Krstic

Dataset, April, 2024

Artifact for "Proactive Real-Time First-Order Enforcement".

François Hublet, Leonardo Lima, David A. Basin, Dmitriy Traytel, Srdan Krstic

Dataset, April, 2024

Artifact for "Proactive Real-Time First-Order Enforcement".

François Hublet, Leonardo Lima, David A. Basin, Srdan Krstic, Dmitriy Traytel

Dataset, April, 2024

A Verified Proof Checker for Metric First-Order Temporal Logic.

Andrei Herasimau, Jonathan Julián Huerta y Munive, Leonardo Lima, Martin Raszyk, Dmitriy Traytel

Arch. Formal Proofs, 2024

Explainable Online Monitoring of Metric First-Order Temporal Logic.

Leonardo Lima, Jonathan Julián Huerta y Munive, Dmitriy Traytel

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

TimelyMon: A Streaming Parallel First-Order Monitor.

Lennard Reese, Rafael Castro G. Silva, Dmitriy Traytel

Proceedings of the Runtime Verification - 24th International Conference, 2024

Proactive Real-Time First-Order Enforcement.

François Hublet, Leonardo Lima, David A. Basin, Srdan Krstic, Dmitriy Traytel

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023

Admissible Types-to-PERs Relativization in Higher-Order Logic.

Andrei Popescu, Dmitriy Traytel

Proc. ACM Program. Lang., January, 2023

Efficient Evaluation of Arbitrary Relational Calculus Queries.

Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel

Log. Methods Comput. Sci., 2023

Pushdown Systems.

Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel

Arch. Formal Proofs, 2023

Labeled Transition Systems.

Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel

Arch. Formal Proofs, 2023

Explainable Online Monitoring of Metric Temporal Logic.

Leonardo Lima, Andrei Herasimau, Martin Raszyk, Dmitriy Traytel, Simon Yuan

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Correct and Efficient Policy Monitoring, a Retrospective.

David A. Basin, Srdan Krstic, Joshua Schneider, Dmitriy Traytel

Proceedings of the Automated Technology for Verification and Analysis, 2023

2022

Quotients of Bounded Natural Functors.

Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel

Log. Methods Comput. Sci., 2022

Making Arbitrary Relational Calculus Queries Safe-Range.

Martin Raszyk, Dmitriy Traytel

Arch. Formal Proofs, 2022

Verified First-Order Monitoring with Recursive Rules.

Sheila Zingg, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

VeriMon: A Formally Verified Monitoring Tool.

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

Proceedings of the Theoretical Aspects of Computing - ICTAC 2022, 2022

Practical Relational Calculus Query Evaluation.

Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel

Proceedings of the 25th International Conference on Database Theory, 2022

Differential Testing of Pushdown Reachability with a Formally Verified Oracle.

Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

2021

Scalable online first-order monitoring.

Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel

Int. J. Softw. Tools Technol. Transf., 2021

A taxonomy for classifying runtime verification tools.

Yliès Falcone, Srdan Krstic, Giles Reger, Dmitriy Traytel

Int. J. Softw. Tools Technol. Transf., 2021

Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant.

Andrei Popescu, Dmitriy Traytel

J. Autom. Reason., 2021

Formalization of Timely Dataflow's Progress Tracking Protocol.

Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel

Arch. Formal Proofs, 2021

Verified Progress Tracking for Timely Dataflow.

Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2020

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.

Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann

J. Autom. Reason., 2020

Syntax-Independent Logic Infrastructure.

Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2020

Robinson Arithmetic.

Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2020

An Abstract Formalization of Gödel's Incompleteness Theorems.

Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2020

From Abstract to Concrete Gödel's Incompleteness Theorems - Part II.

Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2020

From Abstract to Concrete Gödel's Incompleteness Theorems - Part I.

Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2020

Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows.

Lukas Heimes, Dmitriy Traytel, Joshua Schneider

Arch. Formal Proofs, 2020

A Formal Proof of The Chandy-Lamport Distributed Snapshot Algorithm.

Ben Fiedler, Dmitriy Traytel

Arch. Formal Proofs, 2020

Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations.

Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider, Dmitriy Traytel

Arch. Formal Proofs, 2020

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

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Multi-head Monitoring of Metric Dynamic Logic.

Martin Raszyk, David A. Basin, Dmitriy Traytel

Proceedings of the Automated Technology for Verification and Analysis, 2020

2019

Bindings as bounded natural functors.

Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel

Proc. ACM Program. Lang., 2019

Correction to: A survey of challenges for runtime verification from advanced application domains (beyond software).

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

Formal Methods Syst. Des., 2019

A survey of challenges for runtime verification from advanced application domains (beyond software).

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

Formal Methods Syst. Des., 2019

Almost event-rate independent monitoring.

David A. Basin, Bhargav Nagaraja Bhatt, Srdan Krstic, Dmitriy Traytel

Formal Methods Syst. Des., 2019

Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic.

Joshua Schneider, Dmitriy Traytel

Arch. Formal Proofs, 2019

Formalization of Generic Authenticated Data Structures.

Matthias Brun, Dmitriy Traytel

Arch. Formal Proofs, 2019

A Formally Verified Monitor for Metric First-Order Temporal Logic.

Joshua Schneider, David A. Basin, Srdan Krstic, Dmitriy Traytel

Proceedings of the Runtime Verification - 19th International Conference, 2019

Generic Authenticated Data Structures, Formally.

Matthias Brun, Dmitriy Traytel

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

From Nondeterministic to Multi-Head Deterministic Finite-State Transducers.

Martin Raszyk, David A. Basin, Dmitriy Traytel

Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, 2019

A verified prover based on ordered resolution.

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

A Formally Verified Abstract Account of Gödel's Incompleteness Theorems.

Andrei Popescu, Dmitriy Traytel

Proceedings of the Automated Deduction - CADE 27, 2019

Multi-head Monitoring of Metric Temporal Logic.

Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel

Proceedings of the Automated Technology for Verification and Analysis, 2019

Adaptive Online First-Order Monitoring.

Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel

Proceedings of the Automated Technology for Verification and Analysis, 2019

2018

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover.

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel

Arch. Formal Proofs, 2018

Formalization of Bachmair and Ganzinger's Ordered Resolution Prover.

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann

Arch. Formal Proofs, 2018

Optimal Proofs for Linear Temporal Logic on Lasso Words.

David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel

Proceedings of the Automated Technology for Verification and Analysis, 2018

2017

Formal Languages, Formally and Coinductively.

Dmitriy Traytel

Log. Methods Comput. Sci., 2017

Soundness and Completeness Proofs by Coinductive Methods.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

J. Autom. Reason., 2017

Operations on Bounded Natural Functors.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2017

Abstract Soundness.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2017

Almost Event-Rate Independent Monitoring of Metric Temporal Logic.

David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties.

David A. Basin, Srdjan Krstic, Dmitriy Traytel

Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

Almost Event-Rate Independent Monitoring of Metric Dynamic Logic.

David A. Basin, Srdan Krstic, Dmitriy Traytel

Proceedings of the Runtime Verification - 17th International Conference, 2017

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL.

Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

Foundational nonuniform (Co)datatypes for higher-order logic.

Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.

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

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants.

Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel

Proceedings of the Programming Languages and Systems, 2017

A Report of ARCADE 2017.

Giles Reger, Dmitriy Traytel

Proceedings of the ARCADE 2017, 2017

2016

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals.

Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel

Arch. Formal Proofs, 2016

2015

Formalizing Symbolic Decision Procedures for Regular Languages.

Dmytro Traytel

PhD thesis, 2015

Verified decision procedures for MSO on words based on derivatives of regular expressions.

Dmitriy Traytel, Tobias Nipkow

J. Funct. Program., 2015

Foundational Extensible Corecursion.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

CoRR, 2015

Derivatives of Logical Formulas.

Dmitriy Traytel

Arch. Formal Proofs, 2015

A Zoo of Probabilistic Systems.

Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel

Arch. Formal Proofs, 2015

A Formalized Hierarchy of Probabilistic System Types - Proof Pearl.

Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Foundational extensible corecursion: a proof assistant perspective.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Witnessing (Co)datatypes.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Proceedings of the Programming Languages and Systems, 2015

A Coalgebraic Decision Procedure for WS1S.

Dmitriy Traytel

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014

Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions.

Dmitriy Traytel, Tobias Nipkow

Arch. Formal Proofs, 2014

Unified Decision Procedures for Regular Expression Equivalence.

Tobias Nipkow, Dmitriy Traytel

Arch. Formal Proofs, 2014

Abstract Completeness.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Arch. Formal Proofs, 2014

Truly Modular (Co)datatypes for Isabelle/HOL.

Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Cardinals in Isabelle/HOL.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Experience report: the next 1100 Haskell programmers.

Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel

Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, 2014

Unified Classical Logic Completeness - A Coinductive Pearl.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

A Codatatype of Formal Languages.

Dmitriy Traytel

Arch. Formal Proofs, 2013

2012

Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving.

Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

2011

Extending Hindley-Milner Type Inference with Coercive Structural Subtyping.

Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow

Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011