Dmitriy Traytel

Cited by

	All	Since 2019
Citations	1396	1022
h-index	21	17
i10-index	37	31

180

135

20132014201520162017201820192020202120222023202411 37 58 48 131 68 162 152 177 167 180 170

Public access

View all

38 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Jasmin BlanchetteLudwig-Maximilians-Universität MünchenVerified email at ifi.lmu.de
Andrei PopescuUniversity of SheffieldVerified email at sheffield.ac.uk
Srdjan KrsticETH ZurichVerified email at inf.ethz.ch
David BasinProfessor of Computer Science, ETH ZurichVerified email at inf.ethz.ch
Andreas LochbihlerDigital Asset (Switzerland) GmbHVerified email at inf.ethz.ch
Anders SchlichtkrullAalborg University CopenhagenVerified email at cs.aau.dk
Tobias NipkowProfessor of Computer Science, Technische Universität MünchenVerified email at in.tum.de
Johannes HölzlVerified email at in.tum.de
Yliès FalconeUniv. Grenoble Alpes and InriaVerified email at univ-grenoble-alpes.fr
Giles RegerAmazon and University of ManchesterVerified email at manchester.ac.uk
Lorenz PannyTechnische Universität MünchenVerified email at yx7.cc
Bhargav Nagaraja BhattDoctoral Research Assisstant, USI LuganoVerified email at usi.ch
Thibault DardinierETH ZürichVerified email at inf.ethz.ch
Mathias FleuryUniversity FreiburgVerified email at informatik.uni-freiburg.de
Lorenzo GheriUniversity of LiverpoolVerified email at liverpool.ac.uk
Jonathan Julian Huerta y MuniveCzech Technical UniversityVerified email at cvut.cz
Christian SternagelVerified email at uibk.ac.at
Jiri SrbaProfessor of Computer Science, Aalborg UniversityVerified email at cs.aau.dk
Morten Konggaard SchouPostdoc, Aalborg UniversityVerified email at cs.aau.dk
Lars NoschinskiTechnische Universität MünchenVerified email at in.tum.de

Dmitriy Traytel

University of Copenhagen

Verified email at di.ku.dk - Homepage

Interactive Theorem Proving Runtime Verification


Title Sort by citations Sort by year Sort by 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	153	2021
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	125	2014
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	117	2019
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	80	2012
A Formally Verified Monitor for Metric First-Order Temporal Logic J Schneider, D Basin, S Krstić, D Traytel RV, 2019	44	2019
Friends with Benefits: Implementing Foundational Corecursion in Proof Assistants JC Blanchette, A Bouzy, A Lochbihler, A Popescu, D Traytel ESOP 2017, 2017	43*	2017
Soundness and completeness proofs by coinductive methods JC Blanchette, A Popescu, D Traytel Journal of Automated Reasoning 58, 149-179, 2017	43	2017
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	42	2017
Foundational Extensible Corecursion: A Proof Assistant Perspective JC Blanchette, A Popescu, D Traytel ICFP 2015, 192-204, 2015	42	2015
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	39	2020
Unified Classical Logic Completeness—A Coinductive Pearl JC Blanchette, A Popescu, D Traytel IJCAR 2014, 46-60, 2014	39	2014
A verified prover based on ordered resolution A Schlichtkrull, JC Blanchette, D Traytel Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019	37	2019
Unified Decision Procedures for Regular Expression Equivalence T Nipkow, D Traytel ITP 2014, 450-466, 2014	33	2014
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	32	2020
Almost Event-Rate Independent Monitoring of Metric Temporal Logic D Basin, BN Bhatt, D Traytel TACAS 2017, 2017	31	2017
Cardinals in Isabelle/HOL JC Blanchette, A Popescu, D Traytel ITP 2014, 111-127, 2014	30	2014
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping D Traytel, S Berghofer, T Nipkow APLAS 2011, 89-104, 2011	29	2011
Witnessing (Co)datatypes JC Blanchette, A Popescu, D Traytel ESOP 2015, 359-382, 2015	27	2015
AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties. DA Basin, S Krstic, D Traytel RV-CuBES 3, 29-36, 2017	25	2017
Scalable Online First-Order Monitoring J Schneider, D Basin, F Brix, S Krstić, D Traytel International Conference on Runtime Verification, 353-371, 2018	24	2018

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Follow

Cited by

Co-authors