Most cited papers from Runtime Verification (United States)
What are the most cited papers from Runtime Verification (United States)?
The most cited paper from Runtime Verification (United States) is "KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine" (Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues et al., 2018), with 423 citations. Next come "A formal verification tool for Ethereum VM bytecode" (109) and "Semantics-based program verifiers for all languages" (74).
Showing 48 of 48 papers. Every paper is listed.
| # | Paper | ||
|---|---|---|---|
| 1 | KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues et al. | Jul 2018 | 423 |
| 2 | A formal verification tool for Ethereum VM bytecode Daejun Park, Yi Zhang, Manasvi Saxena et al. | 26 Oct 2018 | 109 |
| 3 | Semantics-based program verifiers for all languages Andrei R Stefanescu, Daejun Park, Shijiao Yuwen et al. | 19 Oct 2016 | 74 |
| 4 | A complete formal semantics of x86-64 user-level instruction set architecture Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis et al. | 7 Jun 2019 | 58 |
| 5 | Model-based testing Robert V. Binder, Bruno Legeard, Anne Krämer · Communications of the ACM | 28 Jan 2015 | 37 |
| 6 | End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract Daejun Park, Yi Zhang, Grigore Roşu · Lecture notes in computer science | 2020 | 33 |
| 7 | Checking delay-insensitivity: 10/sup 4/ gates and beyond Alex Kondratyev, Lawrence Neukom, Oriol Roig et al. | 23 Apr 2004 | 30 |
| 8 | Towards a Verified Model of the Algorand Consensus Protocol in Coq Musab A. Alturki, Jing Chen, Victor Luchangco et al. · Lecture notes in computer science | 2020 | 25 |
| 9 | RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial Philip Daian, Ylìès Falcone, Patrick O’Neil Meredith et al. · Lecture notes in computer science | 2015 | 23 |
| 10 | Runtime Verification with the RV System Patrick O’Neil Meredith, Grigore Roşu · Lecture notes in computer science | 2010 | 23 |
| 11 | ApproxTuner Hashim Sharif, Yifan Zhao, Maria Kotsifakou et al. | 17 Feb 2021 | 21 |
| 12 | Statistical Model Checking of RANDAO’s Resilience to Pre-computed Reveal Strategies Musab A. Alturki, Grigore Roşu · Lecture notes in computer science | 2020 | 18 |
| 13 | RV-Match: Practical Semantics-Based Program Analysis Dwight Guth, Chris Hathhorn, Manasvi Saxena et al. · Lecture notes in computer science | 2016 | 18 |
| 14 | Program Verification by Coinduction Brandon M. Moore, Lucas Peña, Grigore Roşu · Lecture notes in computer science | 2018 | 18 |
| 15 | Language-parametric compiler validation with application to LLVM Theodoros Kasampalis, Daejun Park, Zhengyao Lin et al. | 11 Apr 2021 | 17 |
| 16 | Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding Petar Maksimović, Caroline Cronjäger, Andreas Lööw et al. · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) | 2023 | 16 |
| 17 | A general approach to define binders using matching logic Xiaohong Chen, Grigore Roşu · Proceedings of the ACM on Programming Languages | 2 Aug 2020 | 15 |
| 18 | IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain Theodoros Kasampalis, Dwight Guth, Brandon M. Moore et al. · Lecture notes in computer science | 2019 | 15 |
| 19 | Formalizing Correct-by-Construction Casper in Coq Elaine Li, Traian Florin Şerbănuţă, Denisa Diaconescu et al. | May 2020 | 13 |
| 20 | Resource-Bounded Intruders in Denial of Service Attacks Abraão Aires Urquiza, Musab A. Alturki, Max Kanovich et al. | Jun 2019 | 12 |
| 21 | Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda Harold Carr, Christa Jenkins, Mark J. Moir et al. · Lecture notes in computer science | 2022 | 11 |
| 22 | A Language-Independent Approach to Smart Contract Verification Xiaohong Chen, Daejun Park, Grigore Roşu · Lecture notes in computer science | 2018 | 11 |
| 23 | Resource and timing aspects of security protocols Abraão Aires Urquiza, Musab A. Alturki, Tajana Ban Kirigin et al. · Journal of Computer Security | 26 Feb 2021 | 9 |
| 24 | Compositional Symbolic Execution for Correctness and Incorrectness Reasoning Lööw, Andreas, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun et al. · arXiv (Cornell University) | 2024 | 8 |
| 25 | Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk) Grigore Roşu · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) | 2018 | 8 |
| 26 | HPVM: Hardware-Agnostic Programming for Heterogeneous Parallel Systems Adel Ejjeh, Aaron Councilman, Akash Kothari et al. · IEEE Micro | 27 Jun 2022 | 7 |
| 27 | A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich et al. · Lecture notes in computer science | 2019 | 7 |
| 28 | Runtime Verification at Work: A Tutorial Philip Daian, Dwight Guth, Chris Hathhorn et al. · Lecture notes in computer science | 2016 | 7 |
| 29 | A Language-Independent Program Verification Framework Xiaohong Chen, Grigore Roşu · Lecture notes in computer science | 2018 | 6 |
| 30 | All-Path Reachability Logic Andrei R Stefanescu, Ştefan Ciobâcă, Radu Mereuţă et al. · DOAJ (DOAJ: Directory of Open Access Journals) | 2019 | 5 |
| 31 | Model Checking Strategies from Synthesis over Finite Traces Suguman Bansal, Yong Li, Lucas M. Tabajara et al. · Lecture notes in computer science | 2023 | 5 |
| 32 | RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring Philip Daian, Shinichi Shiraishi, Akihito Iwai et al. · SAE technical papers on CD-ROM/SAE technical paper series | 5 Apr 2016 | 5 |
| 33 | On the Formalization and Computational Complexity of Resilience Problems for Cyber-Physical Systems Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich et al. · Lecture notes in computer science | 2022 | 4 |
| 34 | Interactive Matching Logic Proofs in Coq Jan Tušil, Péter Bereczky, Dániel Horpácsi · Lecture notes in computer science | 2023 | 3 |
| 35 | CAE Model Correlation & Design Optimization of a Laminated Steel Oil Pan by means of Acceleration and Strain Measurement on a Fired Engine Rıfat Yanarocak, Abdülkadir Çekiç · International Journal of Engineering Technologies IJET | 16 Jan 2015 | 3 |
| 36 | An Extensible Compiler for Implementing Software Design Patterns as Concise Language Constructs Taher A. Ghaleb, Khalid Aljasser, Musab A. Alturki · International Journal of Software Engineering and Knowledge Engineering | Jul 2021 | 3 |
| 37 | Dealing With C's Original Sin Chris Hathhorn, Grigore Roşu · IEEE Software | 15 Aug 2019 | 3 |
| 38 | Verifying Compliance with the Kyoto Protocol John Lanchbery · Review of European Community & International Environmental Law | Jul 1998 | 3 |
| 39 | Exact Separation Logic (Extended Version) Petar Maksimović, Caroline Cronjäger, Andreas Lööw et al. · arXiv (Cornell University) | 15 Aug 2022 | 2 |
| 40 | The $$\mathbb {K}$$ Vision for the Future of Programming Language Design and Analysis Xiaohong Chen, Grigore Roşu · Lecture notes in computer science | 2021 | 1 |
| 41 | On Security Analysis of Periodic Systems: Expressiveness and Complexity Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich et al. | 2021 | 1 |
| 42 | Compiling by Proving in \({\mathbb{K}}\) : From All-Path Reachability Proofs to Single-Step Semantic Rules Jianhong Zhao, Everett Hildenbrandt, Juan Conejero et al. · ACM Transactions on Software Engineering and Methodology | 28 Jul 2026 | 0 |
| 43 | On-the-fly LTLf Synthesis under Partial Observability Nadav Alon, Supratik Chakraborty, Alexandre Duret-Lutz et al. | Jul 2026 | 0 |
| 44 | A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report Natalia Klaus, Juan Conejero, Palina Tolmach · arXiv (Cornell University) | 28 May 2026 | 0 |
| 45 | EU-UNION Verification European Commission · Zenodo (CERN European Organization for Nuclear Research) | 10 Nov 2025 | 0 |
| 46 | The African Nuclear-Weapon-Free Zone Treaty: A Reflection on the Role of Activism Noël Stott · The Thinker | 4 Oct 2024 | 0 |
| 47 | Asynchronous Muddy Children Puzzle (work in progress) Dafina Trufaș, I. Teodorescu, Denisa Diaconescu et al. · Electronic Proceedings in Theoretical Computer Science | 22 Sep 2023 | 0 |
| 48 | On the Security and Complexity of Periodic Systems Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich et al. · SN Computer Science | 2 Jul 2022 | 0 |
Citations are OpenAlex's own counts, from its 2026-09-23 snapshot, so the ranking can differ from Google Scholar or Web of Science. A paper is listed for an institution when any of its authors gave it as an affiliation; retracted papers and papers whose citation count cannot be traced to citing works are left out, and a preprint and the article it became are shown once. Release dates are OpenAlex's: where a source gave only a month or a year, that is what is shown. How the lists are chosen.