Experts ranked by Total Citation Number.

1 Bertrand Meyer
	H-index: 31; Papers: 127; Citation: 45524   highest-cited paper: Object-Oriented Software Construction, 2nd Edition (1997) (Cited By 6935) Homepage:
Expertise: Software Engineering / Design Patterns Frameworks;   Model Checking / Hybrid Systems;

2 Leslie Lamport (Microsoft Corporation )
	H-index: 54; Papers: 131; Citation: 26067   highest-cited paper: Time, Clocks, and the Ordering of Events in a Distributed System (1978) at Commun. ACM(Cited By 6163) Homepage: http://research.microsoft.com/users/lamport/
Expertise: Dynamic Networks / Extended Abstract;   Model Checking / Hybrid Systems;   Computer / Systems;   Logic Programs / Algebraic Semantics;

3 Nancy A. Lynch (Distributed Algorithms (The Morgan Kaufmann Series in Data Management Systems) Distributed Algorithms (The Morgan Kaufmann Series in Data Management Systems) by Nancy A. Lynch (Hardcover - April 1997))
	H-index: 65; Papers: 251; Citation: 19652   highest-cited paper: Impossibility of Distributed Consensus with One Faulty Process (1985) at J. ACM(Cited By 2866) Homepage: http://people.csail.mit.edu/lynch
Expertise: Dynamic Networks / Extended Abstract;   Finite Languages / Database Queries;   Model Checking / Hybrid Systems;   Communication Complexity / Lower Bounds;   Logic Programs / Algebraic Semantics;   Optimal control;

4 Mihalis Yannakakis ( Professor of Computer Science, Computer Systems Laboratory Dept. of Electrical Engineering School of Engineering Stanford University)
	H-index: 75; Papers: 197; Citation: 18747   highest-cited paper: Optimization, Approximation, and Complexity Classes (1991) at J. Comput. Syst. Sci.(Cited By 1284) Homepage: http://forum.stanford.edu/research/yannakakis.html
Expertise: Communication Complexity / Lower Bounds;   Finite Languages / Database Queries;   Model Checking / Hybrid Systems;   Approximation Algorithms / Perfect Graphs;

5 Amir Pnueli (Faculty of Mathematics and Computer Science, Faculty of Mathematics and Computer Science The Weizmann Institute of Science)
	H-index: 68; Papers: 247; Citation: 17792   highest-cited paper: The Temporal Logic of Programs (1977) at FOCS(Cited By 2529) Homepage: http://www.wisdom.weizmann.ac.il/~amir/
Expertise: Model Checking / Hybrid Systems;   Logic Programs / Algebraic Semantics;   Communication Complexity / Lower Bounds;

6 David Harel (The William Sussman Professorial Chair, Dept. of Computer Science and Applied Mathematics The Weizmann Institute of Science)
	H-index: 54; Papers: 187; Citation: 17021   highest-cited paper: Dynamic logic. (2001) at SIGACT News(Cited By 1580) Homepage: http://www.wisdom.weizmann.ac.il/~harel/
Expertise: Model Checking / Hybrid Systems;   Visual Language;   Finite Languages / Database Queries;   Logic Programs / Algebraic Semantics;   Communication Complexity / Lower Bounds;   Automata Theory / Slender Languages;

7 George C. Necula (Associate Professor , Electrical Engineering and Computer Science Rinera Networks)
	H-index: 29; Papers: 58; Citation: 11847   highest-cited paper: A Scalable Architecture for Proof-Carrying Code (2001) at FLOPS(Cited By 1857) Homepage: http://www.cs.berkeley.edu/~necula/
Expertise: Functional Programming / Binding-Time Analysis;   Model Checking / Hybrid Systems;

8 Zohar Manna (Professor of Computer Science, Computer Science Stanford University,)
	H-index: 59; Papers: 168; Citation: 11664   highest-cited paper: Second-Order Mathematical Theory of Computation (1970) at STOC(Cited By 1120) Homepage: http://theory.stanford.edu/~zm/
Expertise: Model Checking / Hybrid Systems;   Logic Programs / Algebraic Semantics;   Theorem Proving / General-Purpose Automated Reasoning;   Finite Languages / Database Queries;

9 David Garlan (Professor in the School of Computer Science , School of Computer Science at Carnegie Mellon University)
	H-index: 41; Papers: 119; Citation: 11258   highest-cited paper: Errata: A Formal Basis for Architectural Connection (1998) at ACM Trans. Softw. Eng. Methodol.(Cited By 1439) Homepage: http://www.cs.cmu.edu/~garlan/
Expertise: Software Engineering;   Model Checking / Hybrid Systems;   Software Engineering / Business Maintenance Model;   Visual Language;

10 Patrick Cousot ( Professor, Professor of Computer Science)
	H-index: 35; Papers: 69; Citation: 10994   highest-cited paper: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints (1977) at POPL(Cited By 3945) Homepage: http://www.di.ens.fr/~cousot/
Expertise: Functional Programming / Binding-Time Analysis;   Model Checking / Hybrid Systems;

11 Jose Meseguer (Principal Scientist , SRI International, Computer Science Laboratory)
	H-index: 51; Papers: 248; Citation: 10477   highest-cited paper: Security Policies and Security Models (1982) at IEEE Symposium on Security and Privacy(Cited By -1) Homepage: http://www.csl.sri.com/~meseguer
Expertise: Logic Programs / Algebraic Semantics;   Model Checking / Hybrid Systems;   Theorem Proving / General-Purpose Automated Reasoning;   Logic Programs;

12 A. Prasad Sistla (Professor, Department of Computer Science University of Illinois at Chicago )
	H-index: 33; Papers: 96; Citation: 9781   highest-cited paper: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications (1986) at ACM Trans. Program. Lang. Syst.(Cited By 3635) Homepage: http://www.cs.uic.edu/~sistla/
Expertise: Model Checking / Hybrid Systems;   Dynamic Networks / Extended Abstract;   XML Data;

13 Jeff Kramer (Professor , Distributed Software Engineering Department of Computing Imperial College London )
	H-index: 42; Papers: 125; Citation: 8673   highest-cited paper: Specifying Distributed Software Architectures (1995) at ESEC(Cited By 930) Homepage: http://www.doc.ic.ac.uk/~jk/
Expertise: Software Engineering;   Model Checking / Hybrid Systems;

14 Pierre Wolper ( Professor of Computer Science, Universit?? de Liege Institut Montefiore )
	H-index: 35; Papers: 73; Citation: 7979   highest-cited paper: Temporal Logic Can Be More Expressive (1983) at Information and Control(Cited By 640) Homepage: http://www.montefiore.ulg.ac.be/~pw/
Expertise: Model Checking / Hybrid Systems;   Logic Programs / Algebraic Semantics;   Finite Languages / Database Queries;

15 Somesh Jha (Associate Professor, Computer Sciences Department University of Wisconsin)
	H-index: 35; Papers: 99; Citation: 7089   highest-cited paper: Counterexample-guided abstraction refinement for symbolic model checking (2003) at J. ACM(Cited By 1032) Homepage: http://pages.cs.wisc.edu/~jha/
Expertise: Security Views / New Denial;   Model Checking / Hybrid Systems;   Functional Programming / Binding-Time Analysis;   Multi-Agent Systems / Agent organization;   Software Engineering;

16 James B. Saxe
	H-index: 20; Papers: 24; Citation: 6903   highest-cited paper: Extended Static Checking for Java (2002) at PLDI(Cited By 974)
Expertise: Communication Complexity / Lower Bounds;   Model Checking / Hybrid Systems;   Convex Polygons / Planar Arrangements;   Error function / Runge-Kutta integration;   Functional Programming / Binding-Time Analysis;

17 Javier Esparza (Professor, Software Reliability and Security Group Institute for Formal Methods in Computer Science University of Stuttgart)
	H-index: 38; Papers: 115; Citation: 6137   highest-cited paper: Compositional Synthesis of Live and Bounded Free Choice Petri Nets (1991) at CONCUR(Cited By 467) Homepage: http://www7.in.tum.de/~esparza/
Expertise: Logic Programs / Algebraic Semantics;   Petri Nets / Formal Specifications;   Model Checking / Hybrid Systems;   Automata Theory / Slender Languages;   Functional Programming / Binding-Time Analysis;

18 Yuri Gurevich (Yuri GurevichPrincipal Researcher, Microsoft Research;)
	H-index: 37; Papers: 174; Citation: 5895   highest-cited paper: The Classical Decision Problem (1997) (Cited By 528) Homepage: http://research.microsoft.com/~gurevich/
Expertise: Logic Programs / Algebraic Semantics;   Infinitary Logic / Recursive Models;   Finite Languages / Database Queries;   Communication Complexity / Lower Bounds;   Model Checking / Hybrid Systems;

19 David Notkin (Bradley Chair, International Conference on Software Engineering CRA NCWIT)
	H-index: 37; Papers: 122; Citation: 5748   highest-cited paper: Software Reflexion Models: Bridging the Gap Between Source and High-Level Models (1995) at SIGSOFT FSE(Cited By 408) Homepage: http://www.cs.washington.edu/homes/notkin/
Expertise: Software Engineering;   Software Engineering / Business Maintenance Model;   Real-Time Systems / Automated Software Test Data;   Model Checking / Hybrid Systems;   Software Engineering / Design Patterns Frameworks;

20 Bernhard Steffen (Professor, Universit?t Dortmund Fachbereich Informatik )
	H-index: 34; Papers: 138; Citation: 5729   highest-cited paper: The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems (1993) at ACM Trans. Program. Lang. Syst.(Cited By 477) Homepage: http://ls5-www.cs.uni-dortmund.de/LS5/Team/Professoren/Steffen.html
Expertise: Model Checking / Hybrid Systems;   Functional Programming / Binding-Time Analysis;   Logic Programs / Algebraic Semantics;

21 Patrice Godefroid (Software Reliability Research Microsoft Research Microsoft)
	H-index: 39; Papers: 68; Citation: 5697   highest-cited paper: Model Checking for Programming Languages using Verisoft (1997) at POPL(Cited By 507) Homepage: http://research.microsoft.com/users/pg/
Expertise: Model Checking / Hybrid Systems;   Functional Programming / Binding-Time Analysis;   Logic Programs / Algebraic Semantics;

22 Calin Belta
	H-index: 12; Papers: 27; Citation: 5295   highest-cited paper: Robot Motion Planning (2008) at Wiley Encyclopedia of Computer Science and Engineering(Cited By 4938) Homepage: http://iasi.bu.edu/~cbelta/
Expertise: Optimal control;   Mobile Robot / Hybrid Control;   Model Checking / Hybrid Systems;

23 Cormac Flanagan (Associate Professor, Computer Science Department School of Engineering University of California)
	H-index: 34; Papers: 57; Citation: 5281   highest-cited paper: Extended Static Checking for Java (2002) at PLDI(Cited By 974) Homepage: http://www.cse.ucsc.edu/~cormac/
Expertise: Functional Programming / Binding-Time Analysis;   Model Checking / Hybrid Systems;

24 James J. Horning (Chief Scientist, Information Systems Security Operation)
	H-index: 21; Papers: 40; Citation: 4820   highest-cited paper: Learning from experience (2001) at Commun. ACM(Cited By 2933) Homepage: http://home.comcast.net/~jhorning4/
Expertise: Computer / Systems;   Functional Programming / Binding-Time Analysis;   Model Checking / Hybrid Systems;

25 Rance Cleaveland (Professor, Department of Computer Science University of Maryland )
	H-index: 36; Papers: 110; Citation: 4793   highest-cited paper: The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems (1993) at ACM Trans. Program. Lang. Syst.(Cited By 477) Homepage: http://www.cs.umd.edu/~rance/
Expertise: Model Checking / Hybrid Systems;   Logic Programs / Algebraic Semantics;   Software Engineering;

26 K. Rustan M. Leino (principal researcher , Programming Languages and Methods group Microsoft Research)
	H-index: 26; Papers: 68; Citation: 4755   highest-cited paper: Extended Static Checking for Java (2002) at PLDI(Cited By 974) Homepage: https://research.microsoft.com/~leino/
Expertise: Model Checking / Hybrid Systems;   Functional Programming / Binding-Time Analysis;

27 Julian F. Miller ( lecturer , Department of Electronics University of York )
	H-index: 23; Papers: 75; Citation: 4752   highest-cited paper: High efficiency transformation of E. coli by high voltage electroporation (1988) at Nucleic Acids Research(Cited By 1870) Homepage: http://www.elec.york.ac.uk/intsys/users/jfm7/
Expertise: Model Checking / Hybrid Systems;   DNA sequence / ENZYME database;   E-learning Support System / Neural Networks;   Knowledge-based data analysis / Medical Costs;

28 Tobias Nipkow (Institut f??r Informatik Technische Universit?t M??nchen )
	H-index: 37; Papers: 86; Citation: 4669   highest-cited paper: Isabelle/HOL - A Proof Assistant for Higher-Order Logic (2002) (Cited By 493) Homepage: http://www4.in.tum.de/~nipkow/
Expertise: Theorem Proving / General-Purpose Automated Reasoning;   Logic Programs / Algebraic Semantics;   Model Checking / Hybrid Systems;   Functional Programming / Binding-Time Analysis;

29 Reinhard Wilhelm (Chair for Programming Languages and Compiler Construction, Programming Languages and Compiler Construction)
	H-index: 31; Papers: 80; Citation: 4621   highest-cited paper: Parametric shape analysis via 3-valued logic (2002) at ACM Trans. Program. Lang. Syst.(Cited By 729) Homepage: http://rw4.cs.uni-sb.de/index.shtml
Expertise: Functional Programming / Binding-Time Analysis;   Der Informatik / Zur Bedeutung von Modellen;   Real-Time Systems;   Model Checking / Hybrid Systems;   Database Systems / Programming Languages;

30 Sampath Kannan (Professor, Department of Computer and Information Science University of Pennsylvania)
	H-index: 32; Papers: 97; Citation: 4397   highest-cited paper: Designing Programs that Check Their Work (1995) at J. ACM(Cited By 548) Homepage: http://www.cis.upenn.edu/~kannan/
Expertise: Communication Complexity / Lower Bounds;   Approximation Algorithms / Perfect Graphs;   Data Compression / Arithmetic Coding;   Model Checking / Hybrid Systems;   Convex Polygons / Planar Arrangements;

31 Wang Yi (Professor & Director, Research Education Dept. of Information Technology Uppsala University)
	H-index: 30; Papers: 69; Citation: 4379   highest-cited paper: UPPAAL in a Nutshell (1997) at STTT(Cited By 1211) Homepage: http://user.it.uu.se/~yi/
Expertise: Model Checking / Hybrid Systems;   Real-Time Systems;

32 Klaus Havelund (JPL Principal Computer Scientist , Laboratory for Reliable Software (LARS) NASA's Jet Propulsion Laboratory)
	H-index: 28; Papers: 58; Citation: 4368   highest-cited paper: Model Checking Programs (2003) at Autom. Softw. Eng.(Cited By 791) Homepage: http://www.havelund.com/
Expertise: Model Checking / Hybrid Systems;

33 Fabio Somenzi (University of Colorado Dept. of Electrical and Computer Engineering)
	H-index: 37; Papers: 136; Citation: 4319   highest-cited paper: VIS: A System for Verification and Synthesis (1996) at CAV(Cited By 542) Homepage: http://vlsi.colorado.edu/~fabio/
Expertise: Power optimization / Synchronous Sequential Circuits;   Model Checking / Hybrid Systems;   Delay Test / Analysis Replace Fault Simulation;   Low power design / Behavioral Synthesis;

34 Gavin Lowe
	H-index: 10; Papers: 15; Citation: 4298   highest-cited paper: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR (1996) at TACAS(Cited By 1323) Homepage:
Expertise: Security Views / New Denial;   Model Checking / Hybrid Systems;

35 Peter Lee (Professor and Head of Computer Science, Computer Science Carnegie Mellon University)
	H-index: 24; Papers: 46; Citation: 4014   highest-cited paper: Safe Kernel Extensions Without Run-Time Checking (1996) at OSDI(Cited By 636) Homepage: http://www.cs.cmu.edu/~petel/
Expertise: Functional Programming / Binding-Time Analysis;   Model Checking / Hybrid Systems;

36 Rupak Majumdar (Assistant Professor, Computer Science University of California )
	H-index: 32; Papers: 98; Citation: 3949   highest-cited paper: Lazy abstraction (2002) at POPL(Cited By 781) Homepage: http://www.cs.ucla.edu/~rupak/
Expertise: Model Checking / Hybrid Systems;   Functional Programming / Binding-Time Analysis;   Logic Programs / Algebraic Semantics;   Power optimization / Synchronous Sequential Circuits;

37 Pravin Varaiya (Nortel Networks Distinguished Professor, Electrical Engineering and Computer Science University of California, Berkeley)
	H-index: 24; Papers: 62; Citation: 3889   highest-cited paper: Capacity of fading channels with channel side information (1997) at IEEE Transactions on Information Theory(Cited By 1070) Homepage: http://paleale.eecs.berkeley.edu/~varaiya/
Expertise: ATM Networks;   Optimal control;   Model Checking / Hybrid Systems;   Channel state information / Universal coding;   Wireless Networks / Priority Scheduling;   Queueing Networks / Time-dependent performance analysis;

38 Helmut Veith (professor, CS department of Munich Technical University)
	H-index: 21; Papers: 65; Citation: 3855   highest-cited paper: Counterexample-guided abstraction refinement for symbolic model checking (2003) at J. ACM(Cited By 1032) Homepage: http://www7.in.tum.de/~veith/
Expertise: Model Checking / Hybrid Systems;   Logic Programs / Algebraic Semantics;   Communication Complexity / Lower Bounds;   Constraint Programming / Combinatorial Search Problems;   Theorem Proving / General-Purpose Automated Reasoning;

39 Eddie Kohler (assistant professor , UCLA)
	H-index: 24; Papers: 44; Citation: 3828   highest-cited paper: The click modular router (2000) at ACM Trans. Comput. Syst.(Cited By 1229) Homepage: http://www.cs.ucla.edu/~kohler/
Expertise: Wireless network / End-to-end Routing Behavior;   File System / Software Systems;   Sensor Networks / Outdoor wireless;   Wireless Networks / Algorithmic Complexity;   Model Checking / Hybrid Systems;

40 Lintao Zhang (researcher, Microsoft Research Silicon Valley)
	H-index: 15; Papers: 24; Citation: 3773   highest-cited paper: Chaff: Engineering an Efficient SAT Solver (2001) at DAC(Cited By 2302) Homepage: http://research.microsoft.com/users/lintaoz/
Expertise: Constraint Programming / Combinatorial Search Problems;   Power optimization / Synchronous Sequential Circuits;   Model Checking / Hybrid Systems;   File System / Software Systems;

43 Michael D. Ernst (Associate Professor, Program Analysis Group Computer Science & Artificial Intelligence Lab (CSAIL) Dept. of Electrical Engineering & Computer Science Massachusetts Institute of Technology )
	H-index: 27; Papers: 67; Citation: 3543   highest-cited paper: An overview of JML tools and applications (2005) at STTT(Cited By 593) Homepage: http://people.csail.mit.edu/mernst/
Expertise: Software Engineering / Business Maintenance Model;   Software Engineering;   Software Engineering / Design Patterns Frameworks;   Functional Programming / Binding-Time Analysis;   Model Checking / Hybrid Systems;

44 Rajesh K. Gupta (Professor , Department of Computer Science and Engineering University of California)
	H-index: 30; Papers: 137; Citation: 3511   highest-cited paper: Hardware-Software Cosynthesis for Digital Systems (1993) at IEEE Design Test of Computers(Cited By 558) Homepage: http://www.cse.ucsd.edu/~gupta/
Expertise: Delay Test / Analysis Replace Fault Simulation;   Real-Time Systems;   Power optimization / Synchronous Sequential Circuits;   Sensor Networks / Outdoor wireless;   Logic Networks / Fault Simulation;   Model Checking / Hybrid Systems;

45 Ralph-Johan Back (Professor of Computer Science, Computer Science Abo Akademi University)
	H-index: 26; Papers: 76; Citation: 3454   highest-cited paper: Decentralization of Process Nets with Centralized Control (1989) at Distributed Computing(Cited By 0) Homepage: http://www.abo.fi/~backrj/
Expertise: Model Checking / Hybrid Systems;   Logic Programs / Algebraic Semantics;

46 Westley Weimer (Westley Weimer Assistant Professor of Computer Science, Assistant Professor of Computer Science)
	H-index: 13; Papers: 26; Citation: 3437   highest-cited paper: OceanStore: An Architecture for Global-Scale Persistent Storage (2000) at ASPLOS(Cited By 2014) Homepage: http://www.cs.virginia.edu/~weimer/
Expertise: Functional Programming / Binding-Time Analysis;   Real-Time Systems / Automated Software Test Data;   Model Checking / Hybrid Systems;

47 J. Strother Moore (Chair , Computing Theory Department of Computer Sciences )
	H-index: 24; Papers: 53; Citation: 3401   highest-cited paper: A Fast String Searching Algorithm (1977) at Commun. ACM(Cited By 1591) Homepage: http://www.cs.utexas.edu/users/moore/
Expertise: Theorem Proving / General-Purpose Automated Reasoning;   Model Checking / Hybrid Systems;

48 Natarajan Shankar (Staff Scientist)
	H-index: 27; Papers: 37; Citation: 3396   highest-cited paper: Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS (1995) at IEEE Trans. Software Eng.(Cited By 3) Homepage: http://www.csl.sri.com/people/shankar/
Expertise: Model Checking / Hybrid Systems;   Logic Programs / Algebraic Semantics;

49 Willem Visser ( Senior Software Engineer, RIACS (Research Institute for Advanced Computer Science) )
	H-index: 26; Papers: 52; Citation: 3381   highest-cited paper: Model Checking Programs (2003) at Autom. Softw. Eng.(Cited By 791) Homepage: http://ase.arc.nasa.gov/visser/
Expertise: Model Checking / Hybrid Systems;   Multi-Agent Systems / Agent organization;

50 Georges Gonthier (RESEARCHER, Programming Principles and Tools Group )
	H-index: 17; Papers: 27; Citation: 3321   highest-cited paper: The Esterel Synchronous Programming Language: Design, Semantics, Implementation (1992) at Sci. Comput. Program.(Cited By 284) Homepage: http://research.microsoft.com/~gonthier/
Expertise: Logic Programs / Algebraic Semantics;   Functional Programming / Binding-Time Analysis;   Model Checking / Hybrid Systems;