Topic · Formal Methods in Verification
Most cited papers in Formal Methods in Verification
What are the most cited papers in Formal Methods in Verification?
The most cited paper in Formal Methods in Verification is "Petri nets: Properties, analysis and applications" (Tadao Murata, 1989), with 10,641 citations. Next come "Graph-Based Algorithms for Boolean Function Manipulation" (8,956) and "Statecharts: a visual formalism for complex systems" (6,762).
Showing 50 of 98 papers. Every paper with more than 1,172 citations is listed.
| # | Paper | ||
|---|---|---|---|
| 1 | Petri nets: Properties, analysis and applications Tadao Murata · Proceedings of the IEEE | Apr 1989 | 10,641 |
| 2 | Graph-Based Algorithms for Boolean Function Manipulation Bryant · IEEE Transactions on Computers | Aug 1986 | 8,956 |
| 3 | Statecharts: a visual formalism for complex systems David Harel · Science of Computer Programming | Jun 1987 | 6,762 |
| 4 | A theory of timed automata Rajeev Alur, David L. Dill · Theoretical Computer Science | Apr 1994 | 6,524 |
| 5 | Z3: An Efficient SMT Solver Leonardo de Moura, Nikolaj Bjørner · Lecture notes in computer science | 2008 | 6,516 |
| 6 | The temporal logic of programs Amir Pnueli | Sep 1977 | 5,753 |
| 7 | On observing nondeterminism and concurrency Matthew Hennessy, Robin Milner · Lecture notes in computer science | 1980 | 4,501 |
| 8 | Benchmarking optimization software with performance profiles Elizabeth D. Dolan, Jorge J. Morè · Mathematical Programming | 2002 | 4,469 |
| 9 | Planning and acting in partially observable stochastic domains Leslie Pack Kaelbling, Michael L. Littman, Anthony R. Cassandra · Artificial Intelligence | May 1998 | 4,230 |
| 10 | The Unified Modeling Language reference manual James E. Rumbaugh, Grady Booch, Ivar Jacobson · CERN Document Server (European Organization for Nuclear Research) | 1999 | 4,185 |
| 11 | Strips: A new approach to the application of theorem proving to problem solving Richard E. Fikes, Nils J. Nilsson · Artificial Intelligence | Dec 1971 | 4,105 |
| 12 | A logic for default reasoning Raymond Reiter · Artificial Intelligence | Apr 1980 | 3,937 |
| 13 | The model checker SPIN Gerard J. Holzmann · IEEE Transactions on Software Engineering | May 1997 | 3,802 |
| 14 | Communicating sequential processes C. A. R. Hoare · Communications of the ACM | 1983 | 3,789 |
| 15 | Automatic verification of finite-state concurrent systems using temporal logic specifications E. M. Clarke, E. Allen Emerson, Aravinda Prasad Sistla · ACM Transactions on Programming Languages and Systems | Apr 1986 | 3,602 |
| 16 | Supervisory Control of a Class of Discrete Event Processes Peter J. Ramadge, Walter Murray Wonham · SIAM Journal on Control and Optimization | 1987 | 3,372 |
| 17 | A Temporal Logic of Nested Calls and Returns Rajeev Alur, Kousha Etessami, P. Madhusudan · Lecture notes in computer science | 2004 | 3,339 |
| 18 | On the logic of theory change: Partial meet contraction and revision functions Carlos E. Alchourrón, Peter Gärdenfors, David Makinson · Journal of Symbolic Logic | Jun 1985 | 3,248 |
| 19 | A machine program for theorem-proving Martin D. Davis, George W. Logemann, Donald W. Loveland · Communications of the ACM | Jul 1962 | 3,234 |
| 20 | Between MDPs and semi-MDPs: A framework for temporal abstraction in reinforcement learning Richard S. Sutton, Doina Precup, Satinder Pal Singh · Artificial Intelligence | Aug 1999 | 3,216 |
| 21 | The control of discrete event systems Peter J. Ramadge, Walter Murray Wonham · Proceedings of the IEEE | 1989 | 2,945 |
| 22 | Chaff Matthew W. Moskewicz, Conor F. Madigan, Ying Jie Zhao et al. | 2001 | 2,938 |
| 23 | A calculus of mobile processes, I Robin Milner, Joachim Parrow, David S. Walker · Information and Computation | Sep 1992 | 2,867 |
| 24 | Symbolic model checking Emma L. Clarke, K. McMillan, Sérgio Campos et al. · Lecture notes in computer science | 1996 | 2,856 |
| 25 | Constructing Induction Rules for Deductive Synthesis Proofs Alan Bundy, Lucas Dixon, Jeremy Gow et al. · Electronic Notes in Theoretical Computer Science | Mar 2006 | 2,818 |
| 26 | Symbolic model checking: 1020 States and beyond Jerry R. Burch, E. M. Clarke, Kenneth L. McMillan et al. · Information and Computation | Jun 1992 | 2,711 |
| 27 | An Extensible SAT-solver Niklas Eén, Niklas Sörensson · Lecture notes in computer science | 2004 | 2,642 |
| 28 | Can programming be liberated from the von Neumann style? John Backus · Communications of the ACM | Aug 1978 | 2,613 |
| 29 | PRISM 4.0: Verification of Probabilistic Real-Time Systems Marta Kwiatkowska, Gethin Norman, David A. Parker · Lecture notes in computer science | 2011 | 2,390 |
| 30 | Isabelle/HOL: A Proof Assistant for Higher-Order Logic Tobias Nipkow, Markus Wenzel, Lawrence Charles Paulson · Digital Access to Libraries (Université catholique de Louvain (UCL), l'Université de Namur (UNamur) and the Université Saint-Louis (USL-B)) | 2002 | 2,319 |
| 31 | An Algorithm for Subgraph Isomorphism Julian R. Ullmann · Journal of the ACM | 1976 | 2,300 |
| 32 | Design and synthesis of synchronization skeletons using branching time temporal logic Edmund M. Clarke, E. Allen Emerson · Lecture notes in computer science | 19 Nov 2005 | 2,198 |
| 33 | Uppaal in a nutshell Kim G. Larsen, Paul Pettersson, Wang Yi · International Journal on Software Tools for Technology Transfer | Dec 1997 | 2,186 |
| 34 | Symbolic Model Checking without BDDs Armin Biere, Alessandro Cimatti, Edmund M. Clarke et al. · Lecture notes in computer science | 1999 | 2,156 |
| 35 | Attack Detection and Identification in Cyber-Physical Systems Fabio Pasqualetti, Florian Dörfler, Francesco Bullo · IEEE Transactions on Automatic Control | 21 Jun 2013 | 2,131 |
| 36 | Symbolic Boolean manipulation with ordered binary-decision diagrams Randal E. Bryant · ACM Computing Surveys | Sep 1992 | 2,030 |
| 37 | A Structural Approach to Operational Semantics Gordon D. Plotkin | 2004 | 1,983 |
| 38 | Temporal and Modal Logic E. Allen Emerson · Elsevier eBooks | 1990 | 1,913 |
| 39 | The algorithmic analysis of hybrid systems Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs et al. · Theoretical Computer Science | Feb 1995 | 1,889 |
| 40 | The theory of hybrid automata Thomas A. Henzinger | 23 Dec 2002 | 1,861 |
| 41 | Proof-carrying code George C. Necula | 1997 | 1,838 |
| 42 | Binary Decision Diagrams Akers · IEEE Transactions on Computers | Jun 1978 | 1,834 |
| 43 | The complexity of satisfiability problems Thomas J. Schaefer | 1978 | 1,769 |
| 44 | A Formal Analysis and Taxonomy of Task Allocation in Multi-Robot Systems Brian P. Gerkey, Maja J. Matarić · The International Journal of Robotics Research | Sep 2004 | 1,745 |
| 45 | The Esterel synchronous programming language: design, semantics, implementation Gérard Berry, Georges Gonthier · Science of Computer Programming | Nov 1992 | 1,734 |
| 46 | Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks Guy Katz, Clark Barrett, David L. Dill et al. · Lecture notes in computer science | 2017 | 1,718 |
| 47 | Notions of computation and monads Eugenio Moggi · Information and Computation | Jul 1991 | 1,716 |
| 48 | Counterexample-Guided Abstraction Refinement Edmund M. Clarke, Orna Grümberg, Somesh Jha et al. · Lecture notes in computer science | 2000 | 1,707 |
| 49 | On understanding types, data abstraction, and polymorphism Luca Cardelli, Peter W. Wegner · ACM Computing Surveys | 10 Dec 1985 | 1,675 |
| 50 | Control Under Communication Constraints Sekhar Tatikonda, Sanjoy K. Mitter · IEEE Transactions on Automatic Control | Jul 2004 | 1,674 |
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 a field when OpenAlex files it under one of the field's topics; 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.