Kenneth L. Mcmillan

Kenneth L. Mcmillan's AcademicInfluence.com Rankings

Kenneth L. Mcmillan

Computer Science

#4801

World Rank

#5067

Historical Rank

Database

#1992

World Rank

#2090

Historical Rank

computer-science Degrees

Download Badge

Computer Science

Kenneth L. Mcmillan's Degrees

PhD Computer Science Stanford University
Masters Computer Science Stanford University
Bachelors Computer Science Stanford University

Similar Degrees You Can Earn

Why Is Kenneth L. Mcmillan Influential?

(Suggest an Edit or Addition)

(See a Problem?)

Kenneth L. Mcmillan's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

Symbolic model checking (1993) (3679)
Symbolic Model Checking: 10^20 States and Beyond (1990) (3253)
Symbolic model checking: an approach to the state explosion problem (1992) (1304)
Interpolation and SAT-Based Model Checking (2003) (945)
Symbolic model checking for sequential circuit verification (1993) (597)
Compositional model checking (1989) (549)
Sequential circuit verification using symbolic model checking (1990) (483)
Lazy Abstraction with Interpolants (2006) (464)
Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits (1992) (438)
Abstractions from proofs (2004) (422)
Theory of latency-insensitive design (2001) (402)
Applying SAT Methods in Unbounded Symbolic Model Checking (2002) (385)
Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping (1993) (348)
A technique of state space search based on unfolding (1995) (319)
Verification of the Futurebus+ cache coherence protocol (1993) (315)
An interpolating theorem prover (2005) (298)
Automatic Veriication of Nite-state Concurrent Systems Using Temporal-logic Speciications. Acm (1993) (295)
A structural induction theorem for processes (1989) (289)
The SMV System (1993) (287)
Efficient generation of counterexamples and witnesses in symbolic model checking (1995) (255)
Automatic Abstraction without Counterexamples (2003) (252)
Horn Clause Solvers for Program Verification (2015) (202)
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking (1998) (194)
A Practical and Complete Approach to Predicate Refinement (2006) (189)
Verification of Infinite State Systems by Compositional Model Checking (1999) (185)
A methodology for correct-by-construction latency insensitive design (1999) (172)
A Compositional Rule for Hardware Design Refinement (1997) (169)
Symbolic Model Checking : IO * ’ States and Beyond * (1992) (167)
Ivy: safety verification by interactive generalization (2016) (162)
A methodology for hardware verification using compositional model checking (2000) (156)
Quantified Invariant Generation Using an Interpolating Saturation Prover (2008) (154)
Applications of Craig Interpolants in Model Checking (2005) (136)
Inductive invariant generation via abductive inference (2013) (136)
Algorithms for interface timing verification (1992) (134)
Model-checking of correctness conditions for concurrent objects (1996) (131)
Lazy Annotation for Program Testing and Verification (2010) (130)
Differential assertion checking (2013) (126)
On Solving Universally Quantified Horn Clauses (2013) (125)
An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment (2005) (125)
Abstractions from proofs (2004) (122)
Array Abstractions from Proofs (2007) (121)
Fast discrete function evaluation using decision diagrams (1995) (120)
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking (2001) (117)
Interpolant-Based Transition Relation Approximation (2005) (110)
Microarchitecture Verification by Compositional Model Checking (2001) (107)
Analysis of digital circuits through symbolic reduction (1991) (104)
Approximation and decomposition of binary decision diagrams (1998) (80)
A language for compositional specification and verification of finite state hardware controllers (1991) (80)
Automated assumption generation for compositional verification (2007) (80)
Program Verification as Satisfiability Modulo Theories (2013) (78)
Beautiful Interpolants (2013) (78)
Interpolants from Z3 proofs (2011) (67)
Safe BDD Minimization Using Don't Cares (1997) (64)
Generalizing DPLL to Richer Logics (2009) (62)
Latency Insensitive Protocols (1999) (59)
Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study (1995) (56)
Circular Compositional Reasoning about Liveness (1999) (56)
Minimum Satisfying Assignments for SMT (2012) (55)
Experimental Analysis of Different Techniques for Bounded Model Checking (2003) (54)
Induction in Compositional Model Checking (2000) (52)
Solving Constrained Horn Clauses using Interpolation (2013) (51)
Modularity for decidability of deductive verification with applications to distributed systems (2018) (49)
Lazy Annotation Revisited (2014) (42)
Synthesizing converters between finite state protocols (1991) (41)
Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings (1995) (40)
Applications of Craig Interpolation to Model Checking (2004) (38)
Probabilistic state space search (1999) (37)
Symbolic model checking: 10/sup 20/ states and beyond (1990) (37)
Compositional verification of procedural programs using horn clauses over integers and arrays (2015) (37)
A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking (1996) (34)
Formal specification and testing of QUIC (2019) (34)
A Hybrid of Counterexample-Based and Proof-Based Abstraction (2004) (34)
Fitting Formal Methods into the Design Cycle (1994) (32)
Computing Relational Fixed Points using Interpolation (2013) (28)
Hierarchical Representations of Discrete Functions, with Application to Model Checking (1994) (27)
Synthesis of circular compositional program proofs via abduction (2013) (25)
Interpolation and Model Checking (2018) (24)
The smv system draft (1992) (24)
Ivy: A Multi-modal Verification Tool for Distributed Algorithms (2020) (23)
Deciding Global Partial-Order Properties (1998) (22)
Deductive Verification in Decidable Fragments with Ivy (2018) (20)
Engineering change in a non-deterministic FSM setting (1996) (18)
Sibling-substitution-based BDD minimization using don't cares (2000) (18)
Interpolants and Symbolic Model Checking (2007) (17)
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types (2013) (17)
Don’t-Care Computation using k-clause Approximation (2005) (16)
Combining Abstraction Refinement and SAT-Based Model Checking (2007) (16)
Liveness by Invisible Invariants (2006) (14)
Modular specification and verification of a cache-coherent interface (2016) (14)
Temporal prophecy for proving temporal properties of infinite-state systems (2018) (14)
Invisible Invariants and Abstract Interpretation (2011) (11)
Logic for Programming, Artificial Intelligence, and Reasoning (2013) (10)
Methods for exploiting SAT solvers in unbounded model checking (2003) (9)
Craig Interpolation and Reachability Analysis (2003) (9)
Relevance heuristics for program analysis (2008) (8)
Learning Abstractions for Program Synthesis (2018) (7)
Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract) (1998) (5)
Eager Abstraction for Symbolic Model Checking (2018) (5)
Widening and Interpolation (2011) (5)
Heuristic Symmetry Reduction for Invariant Verification (2007) (4)
Complex system verification (panel): the challenge ahead (1994) (4)
Temporal Logic and Model Checking (2000) (4)
Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings (2014) (3)
Invisible Invariants Are Neither (2019) (3)
Program Verication as Satisability Modulo Theories (2012) (3)
Abstract Counterexamples for Non-disjunctive Abstractions (2009) (3)
Interpolation : Proofs in the Service of Model Checking (2011) (3)
Compositional Testing of Internet Protocols (2019) (3)
NeuroComb: Improving SAT Solving with Graph Neural Networks (2021) (3)
P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols (2018) (2)
Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials (2012) (2)
Proof Rules for Model Checking Systems with Data (1998) (2)
A Partial Order Approach (1993) (2)
Induction duality: primal-dual search for invariants (2022) (2)
Automatic verification of sequential circuit designs. Discussion (1992) (2)
Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8318 (2014) (1)
Model checking (2003) (1)
5 Conclusion and Future Work 4 Experimental Results (1995) (1)
Compositional Systems and Methods (2000) (1)
Improved Model Checking Techniques for State Space Analysis of Gene Regulatory Networks (2010) (1)
Symmetry and Model Checking (2000) (1)
What's in Common between Test, Model Checking, and Decision Procedures? (2009) (1)
3.3 Parallel Programs (2011) (0)
Proofs, Interpolants, and Relevance Heuristics (2009) (0)
A Distributed Cache Protocol (1993) (0)
Overview of Verification (2000) (0)
Tutorial on Static Inference of Numeric (2017) (0)
SymMC: approximate model enumeration and counting using symmetry information for Alloy specifications (2022) (0)
Deductive Generalization (2013) (0)
An Engineering Change Methodology Using Simulation Relations. (1999) (0)
Improving SAT Solving with Graph Neural Networks (2021) (0)
5.2 Gate Level Veriication 4.2 Model Checking 4.1 Symbolic Simulation Fitting Formal Methods into the Design Cycle (1994) (0)
Figure 15: a Run of the Bouncing-ball Automaton Automatic Veriication of Nite-state Con- Current Systems Using Temporal-logic Speciications. Acm Transactions on Programming Figure 13: Two-pass Approximative Analysis down up Y 0 Z 0 (1994) (0)
Formal Methods in Computer-Aided Design (2002) (0)
Mu-Calculus Model Checking (1993) (0)
Model Checking 4 Extensions Next-time Operator 3 Decision Procedure for Istl 2 a Global Partial-order Logic Deciding Global Partial-order Properties (0)
LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings (2014) (0)
Formal Property Verification (2016) (0)
Tctl with Freeze Quantiiers Complexity of Reasoning about Real-time (1993) (0)
Reasoning about Network Topologies in Space (2014) (0)
6 Experimental Results and Conclusions 5 Comparison with Previous Work (1995) (0)
Getting started with SMVK (2011) (0)
Toward Property-Driven Abstraction for Heap Manipulating Programs (2007) (0)
Induction and Model Checking (1993) (0)
Synthesizing History and Prophecy Variables for Symbolic Model Checking (2023) (0)
Lemma 4 given 0 = S 0 0 S 0 #cell #nodes #time(sec) Trans. #reachable States #cell #nodes #time(sec) Trans. #reachable States (1994) (0)
Bayesian Interpolants as Explanations for Neural Inferences (2020) (0)
6. Symbolic Model Checking (2000) (0)
Some strategies for proving theorems with a model checker abstract of invited talk (2000) (0)
Verification, Model Checking, and Abstract Interpretation (2014) (0)
Solving Constrained Horn Clauses using Interpolation MSR-TR-2013-6 (2013) (0)
Figure 3: Microprocessor Speciication Bolic Model Checking for Sequential Circuit Veriication. Ieee Transactions on 5 Conclusions and Future Work 4.2 Abstracting the Microprocessor Design 4.1 Proving the Lemmas Using Model-checking (0)
Eecient Regression Veriication (1996) (0)
Verifying cache coherence protocols (1996) (0)