| 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 | 146 | 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 | 124 | 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 | 106 | 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 | 41* | 2017 |
| Soundness and completeness proofs by coinductive methods JC Blanchette, A Popescu, D Traytel Journal of Automated Reasoning 58, 149-179, 2017 | 40 | 2017 |
| Foundational Extensible Corecursion: A Proof Assistant Perspective JC Blanchette, A Popescu, D Traytel ICFP 2015, 192-204, 2015 | 40 | 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 |
| 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 | 39 | 2017 |
| Unified Classical Logic Completeness—A Coinductive Pearl JC Blanchette, A Popescu, D Traytel IJCAR 2014, 46-60, 2014 | 38 | 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 | 34 | 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 | 31 | 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 | 29 | 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 | 24 | 2017 |
| Scalable Online First-Order Monitoring J Schneider, D Basin, F Brix, S Krstić, D Traytel International Conference on Runtime Verification, 353-371, 2018 | 22 | 2018 |
Jasmin BlanchetteLudwig-Maximilians-Universität München在 ifi.lmu.de 的电子邮件经过验证
