Dmitriy Traytel

99 papers A* 3A 8B 25C 2Journal 47Unranked 13

Year	Rank	Type	Title / Venue / Authors
2025	B	`conf`	Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. ITP Jan van Brügge, Andrei Popescu, Dmitriy Traytel
2025	J	`jnl`	Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings. Proc. ACM Program. Lang. Jan van Brügge, James McKinna, Andrei Popescu, Dmitriy Traytel
2025	J	`jnl`	Formalization of (Conflict-)Serializability and Strict Two-Phase Locking. Arch. Formal Proofs Dmitriy Traytel
2025	B	`conf`	Nondeterministic Asynchronous Dataflow in Isabelle/HOL. ITP Rafael Castro Gonçalves Silva, Laouen Fernet, Dmitriy Traytel
2025	—	`conf`	Scaling Up Proactive Enforcement. CAV (3) François Hublet, Leonardo Lima, David A. Basin, Srdan Krstic, Dmitriy Traytel
2024	J	`jnl`	A Verified Proof Checker for Metric First-Order Temporal Logic. Arch. Formal Proofs Andrei Herasimau, Jonathan Julián Huerta y Munive, Leonardo Lima, Martin Raszyk, Dmitriy Traytel
2024	—	`conf`	Explainable Online Monitoring of Metric First-Order Temporal Logic. TACAS (1) Leonardo Lima, Jonathan Julián Huerta y Munive, Dmitriy Traytel
2024	—	`conf`	Proactive Real-Time First-Order Enforcement. CAV (2) François Hublet, Leonardo Lima, David A. Basin, Srdan Krstic, Dmitriy Traytel
2024	B	`ed.`	Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024 CPP Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy
2024	B	`conf`	TimelyMon: A Streaming Parallel First-Order Monitor. RV Lennard Reese, Rafael Castro Gonçalves Silva, Dmitriy Traytel
2024	—	`conf`	WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts. ATVA (2) Leonardo Lima, Jonathan Julián Huerta y Munive, Dmitriy Traytel
2023	J	`jnl`	Admissible Types-to-PERs Relativization in Higher-Order Logic. Proc. ACM Program. Lang. Andrei Popescu, Dmitriy Traytel
2023	—	`conf`	Correct and Efficient Policy Monitoring, a Retrospective. ATVA (1) David A. Basin, Srdan Krstic, Joshua Schneider, Dmitriy Traytel
2023	J	`jnl`	Efficient Evaluation of Arbitrary Relational Calculus Queries. Log. Methods Comput. Sci. Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel
2023	—	`conf`	Explainable Online Monitoring of Metric Temporal Logic. TACAS (2) Leonardo Lima, Andrei Herasimau, Martin Raszyk, Dmitriy Traytel, Simon Yuan
2023	J	`jnl`	Labeled Transition Systems. Arch. Formal Proofs Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel
2023	B	`ed.`	Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023 CPP Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic
2023	J	`jnl`	Pushdown Systems. Arch. Formal Proofs Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel
2022	B	`conf`	Differential Testing of Pushdown Reachability with a Formally Verified Oracle. FMCAD Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel
2022	J	`jnl`	Efficient Evaluation of Arbitrary Relational Calculus Queries. CoRR Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel
2022	J	`jnl`	Making Arbitrary Relational Calculus Queries Safe-Range. Arch. Formal Proofs Martin Raszyk, Dmitriy Traytel
2022	A	`conf`	Practical Relational Calculus Query Evaluation. ICDT Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel
2022	J	`jnl`	Quotients of Bounded Natural Functors. Log. Methods Comput. Sci. Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
2022	C	`conf`	VeriMon: A Formally Verified Monitoring Tool. ICTAC 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
2022	—	`conf`	Verified First-Order Monitoring with Recursive Rules. TACAS (2) Sheila Zingg, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
2021	J	`jnl`	A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf. Yliès Falcone, Srdan Krstic, Giles Reger, Dmitriy Traytel
2021	J	`jnl`	Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant. J. Autom. Reason. Andrei Popescu, Dmitriy Traytel
2021	J	`jnl`	Formalization of Timely Dataflow's Progress Tracking Protocol. Arch. Formal Proofs Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel
2021	J	`jnl`	Quotients of Bounded Natural Functors. CoRR Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
2021	J	`jnl`	Scalable online first-order monitoring. Int. J. Softw. Tools Technol. Transf. Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel
2021	B	`conf`	Verified Progress Tracking for Timely Dataflow. ITP Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel
2020	J	`jnl`	A Formal Proof of The Chandy-Lamport Distributed Snapshot Algorithm. Arch. Formal Proofs Ben Fiedler, Dmitriy Traytel
2020	—	`conf`	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic. IJCAR (1) David A. Basin, Thibault Dardinier, Lukas Heimes, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
2020	J	`jnl`	An Abstract Formalization of Gödel's Incompleteness Theorems. Arch. Formal Proofs Andrei Popescu, Dmitriy Traytel
2020	J	`jnl`	Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows. Arch. Formal Proofs Lukas Heimes, Dmitriy Traytel, Joshua Schneider
2020	J	`jnl`	Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations. Arch. Formal Proofs Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
2020	J	`jnl`	Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. J. Autom. Reason. Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann
2020	J	`jnl`	From Abstract to Concrete Gödel's Incompleteness Theorems - Part I. Arch. Formal Proofs Andrei Popescu, Dmitriy Traytel
2020	J	`jnl`	From Abstract to Concrete Gödel's Incompleteness Theorems - Part II. Arch. Formal Proofs Andrei Popescu, Dmitriy Traytel
2020	B	`conf`	Multi-head Monitoring of Metric Dynamic Logic. ATVA Martin Raszyk, David A. Basin, Dmitriy Traytel
2020	—	`conf`	Quotients of Bounded Natural Functors. IJCAR (2) Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
2020	J	`jnl`	Robinson Arithmetic. Arch. Formal Proofs Andrei Popescu, Dmitriy Traytel
2020	J	`jnl`	Syntax-Independent Logic Infrastructure. Arch. Formal Proofs Andrei Popescu, Dmitriy Traytel
2019	A	`conf`	A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. CADE Andrei Popescu, Dmitriy Traytel
2019	B	`conf`	A Formally Verified Monitor for Metric First-Order Temporal Logic. RV Joshua Schneider, David A. Basin, Srdan Krstic, Dmitriy Traytel
2019	J	`jnl`	A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des. 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
2019	B	`conf`	A verified prover based on ordered resolution. CPP Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel
2019	B	`conf`	Adaptive Online First-Order Monitoring. ATVA Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel
2019	J	`jnl`	Almost event-rate independent monitoring. Formal Methods Syst. Des. David A. Basin, Bhargav Nagaraja Bhatt, Srdan Krstic, Dmitriy Traytel
2019	J	`jnl`	Bindings as bounded natural functors. Proc. ACM Program. Lang. Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel
2019	J	`jnl`	Correction to: A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des. 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
2019	J	`jnl`	Formalization of Generic Authenticated Data Structures. Arch. Formal Proofs Matthias Brun, Dmitriy Traytel
2019	J	`jnl`	Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic. Arch. Formal Proofs Joshua Schneider, Dmitriy Traytel
2019	A*	`conf`	From Nondeterministic to Multi-Head Deterministic Finite-State Transducers. ICALP Martin Raszyk, David A. Basin, Dmitriy Traytel
2019	B	`conf`	Generic Authenticated Data Structures, Formally. ITP Matthias Brun, Dmitriy Traytel
2019	B	`conf`	Multi-head Monitoring of Metric Temporal Logic. ATVA Martin Raszyk, David A. Basin, Srdan Krstic, Dmitriy Traytel
2018	J	`jnl`	A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software). CoRR 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
2018	B	`conf`	A Taxonomy for Classifying Runtime Verification Tools. RV Yliès Falcone, Srdan Krstic, Giles Reger, Dmitriy Traytel
2018	J	`jnl`	A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel
2018	J	`jnl`	Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann
2018	A	`conf`	Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. IJCAR Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann
2018	B	`conf`	Optimal Proofs for Linear Temporal Logic on Lasso Words. ATVA David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel
2018	B	`conf`	Scalable Online First-Order Monitoring. RV Joshua Schneider, David A. Basin, Frederik Brix, Srdan Krstic, Dmitriy Traytel
2017	—	`conf`	A Report of ARCADE 2017. ARCADE@CADE Giles Reger, Dmitriy Traytel
2017	—	`conf`	AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties. RV-CuBES David A. Basin, Srdjan Krstic, Dmitriy Traytel
2017	—	`ed.`	ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017 ARCADE@CADE Giles Reger, Dmitriy Traytel
2017	J	`jnl`	Abstract Soundness. Arch. Formal Proofs Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2017	B	`conf`	Almost Event-Rate Independent Monitoring of Metric Dynamic Logic. RV David A. Basin, Srdan Krstic, Dmitriy Traytel
2017	—	`conf`	Almost Event-Rate Independent Monitoring of Metric Temporal Logic. TACAS (2) David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel
2017	J	`jnl`	Formal Languages, Formally and Coinductively. Log. Methods Comput. Sci. Dmitriy Traytel
2017	—	`conf`	Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS 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
2017	A*	`conf`	Foundational nonuniform (Co)datatypes for higher-order logic. LICS Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel
2017	A	`conf`	Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel
2017	B	`conf`	Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. FSCD Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
2017	J	`jnl`	Operations on Bounded Natural Functors. Arch. Formal Proofs Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2017	J	`jnl`	Soundness and Completeness Proofs by Coinductive Methods. J. Autom. Reason. Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2016	B	`conf`	Formal Languages, Formally and Coinductively. FSCD Dmitriy Traytel
2016	J	`jnl`	Formal Languages, Formally and Coinductively. CoRR Dmitriy Traytel
2016	J	`jnl`	Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. Arch. Formal Proofs Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel
2015	B	`conf`	A Coalgebraic Decision Procedure for WS1S. CSL Dmitriy Traytel
2015	B	`conf`	A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. ITP Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel
2015	J	`jnl`	A Zoo of Probabilistic Systems. Arch. Formal Proofs Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel
2015	J	`jnl`	Derivatives of Logical Formulas. Arch. Formal Proofs Dmitriy Traytel
2015	J	`jnl`	Foundational Extensible Corecursion. CoRR Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2015	A	`conf`	Foundational extensible corecursion: a proof assistant perspective. ICFP Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2015	J	`jnl`	Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. Dmitriy Traytel, Tobias Nipkow
2015	A	`conf`	Witnessing (Co)datatypes. ESOP Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2014	J	`jnl`	Abstract Completeness. Arch. Formal Proofs Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2014	B	`conf`	Cardinals in Isabelle/HOL. ITP Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2014	J	`jnl`	Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions. Arch. Formal Proofs Dmitriy Traytel, Tobias Nipkow
2014	C	`conf`	Experience report: the next 1100 Haskell programmers. Haskell Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel
2014	B	`conf`	Truly Modular (Co)datatypes for Isabelle/HOL. ITP Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel
2014	A	`conf`	Unified Classical Logic Completeness - A Coinductive Pearl. IJCAR Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
2014	B	`conf`	Unified Decision Procedures for Regular Expression Equivalence. ITP Tobias Nipkow, Dmitriy Traytel
2014	J	`jnl`	Unified Decision Procedures for Regular Expression Equivalence. Arch. Formal Proofs Tobias Nipkow, Dmitriy Traytel
2013	J	`jnl`	A Codatatype of Formal Languages. Arch. Formal Proofs Dmitriy Traytel
2013	A	`conf`	Verified decision procedures for MSO on words based on derivatives of regular expressions. ICFP Dmitriy Traytel, Tobias Nipkow
2012	A*	`conf`	Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. LICS Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette
2011	B	`conf`	Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. APLAS Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow