Follow
Dmitriy Traytel
Title
Cited by
Cited by
Year
A taxonomy for classifying runtime verification tools
Y Falcone, S Krstiæ, G Reger, D Traytel
International Journal on Software Tools for Technology Transfer 23 (2), 255-284, 2021
1542021
Truly Modular (Co)datatypes for Isabelle/HOL
JC Blanchette, J Hölzl, A Lochbihler, L Panny, A Popescu, D Traytel
ITP 2014, 93-110, 2014
1262014
A survey of challenges for runtime verification from advanced application domains (beyond software)
C Sánchez, G Schneider, W Ahrendt, E Bartocci, D Bianculli, C Colombo, ...
Formal Methods in System Design 54, 279-335, 2019
1172019
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
D Traytel, A Popescu, JC Blanchette
LICS 2012, 596-605, 2012
812012
A Formally Verified Monitor for Metric First-Order Temporal Logic
J Schneider, D Basin, S Krstiæ, D Traytel
RV, 2019
442019
Friends with Benefits: Implementing Foundational Corecursion in Proof Assistants
JC Blanchette, A Bouzy, A Lochbihler, A Popescu, D Traytel
ESOP 2017, 2017
44*2017
Soundness and completeness proofs by coinductive methods
JC Blanchette, A Popescu, D Traytel
Journal of Automated Reasoning 58, 149-179, 2017
432017
Foundational Extensible Corecursion: A Proof Assistant Perspective
JC Blanchette, A Popescu, D Traytel
ICFP 2015, 192-204, 2015
432015
Almost event-rate independent monitoring of metric dynamic logic
D Basin, S Krstiæ, D Traytel
Runtime Verification: 17th International Conference, RV 2017, Seattle, WA …, 2017
422017
A formally verified, optimized monitor for metric first-order dynamic logic
D Basin, T Dardinier, S Krstic, L Heimes, M Raszyk, J Schneider, D Traytel
IJCAR 2020, 2020
392020
Unified Classical Logic Completeness—A Coinductive Pearl
JC Blanchette, A Popescu, D Traytel
IJCAR 2014, 46-60, 2014
392014
A verified prover based on ordered resolution
A Schlichtkrull, JC Blanchette, D Traytel
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
372019
Unified Decision Procedures for Regular Expression Equivalence
T Nipkow, D Traytel
ITP 2014, 450-466, 2014
332014
Formalizing Bachmair and Ganzinger’s ordered resolution prover
A Schlichtkrull, J Blanchette, D Traytel, U Waldmann
Journal of Automated Reasoning 64 (7), 1169-1195, 2020
322020
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
D Basin, BN Bhatt, D Traytel
TACAS 2017, 2017
312017
Cardinals in Isabelle/HOL
JC Blanchette, A Popescu, D Traytel
ITP 2014, 111-127, 2014
302014
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping
D Traytel, S Berghofer, T Nipkow
APLAS 2011, 89-104, 2011
292011
Witnessing (Co)datatypes
JC Blanchette, A Popescu, D Traytel
ESOP 2015, 359-382, 2015
272015
AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties.
DA Basin, S Krstic, D Traytel
RV-CuBES 3, 29-36, 2017
252017
Scalable Online First-Order Monitoring
J Schneider, D Basin, F Brix, S Krstiæ, D Traytel
International Conference on Runtime Verification, 353-371, 2018
242018
The system can't perform the operation now. Try again later.
Articles 1–20