| 2024 | CAV | Toward Liveness Proofs at Scale. | Kenneth L. McMillan |
| 2024 | ICLR | NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks. | Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth L. McMillan, Risto Miikkulainen |
| 2023 | VMCAI | Synthesizing History and Prophecy Variables for Symbolic Model Checking. | Cole Vick, Kenneth L. McMillan |
| 2020 | CAV | Ivy: A Multi-modal Verification Tool for Distributed Algorithms. | Kenneth L. McMillan, Oded Padon |
| 2019 | SIGCOMM | Formal specification and testing of QUIC. | Kenneth L. McMillan, Lenore D. Zuck |
| 2018 | CAV | Eager Abstraction for Symbolic Model Checking. | Kenneth L. McMillan |
| 2018 | CAV | Learning Abstractions for Program Synthesis. | Xinyu Wang, Greg Anderson, Isil Dillig, Kenneth L. McMillan |
| 2018 | FMCAD | Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. | Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham |
| 2018 | PLDI | Modularity for decidability of deductive verification with applications to distributed systems. | Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos |
| 2018 | SAS | Deductive Verification in Decidable Fragments with Ivy. | Kenneth L. McMillan, Oded Padon |
| 2018 | VMCAI | P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols. | Lenore D. Zuck, Kenneth L. McMillan, Jordan Torf |
| 2016 | FMCAD | Modular specification and verification of a cache-coherent interface. | Kenneth L. McMillan |
| 2016 | PLDI | Ivy: safety verification by interactive generalization. | Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham |
| 2015 | FMCAD | Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. | Anvesh Komuravelli, Nikolaj S. Bjrner, Arie Gurfinkel, Kenneth L. McMillan |
| 2014 | CAV | Lazy Annotation Revisited. | Kenneth L. McMillan |
| 2013 | CAV | Beautiful Interpolants. | Aws Albarghouthi, Kenneth L. McMillan |
| 2013 | OOPSLA | Inductive invariant generation via abductive inference. | Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan |
| 2013 | SAS | On Solving Universally Quantified Horn Clauses. | Nikolaj S. Bjrner, Kenneth L. McMillan, Andrey Rybalchenko |
| 2013 | TACAS | Synthesis of Circular Compositional Program Proofs via Abduction. | Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv |
| 2012 | CADE | Program Verification as Satisfiability Modulo Theories. | Nikolaj S. Bjrner, Kenneth L. McMillan, Andrey Rybalchenko |
| 2012 | CAV | Minimum Satisfying Assignments for SMT. | Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken |
| 2011 | FMCAD | Interpolants from Z3 proofs. | Kenneth L. McMillan |
| 2011 | SAS | Widening and Interpolation. | Kenneth L. McMillan |
| 2011 | SAS | Invisible Invariants and Abstract Interpretation. | Kenneth L. McMillan, Lenore D. Zuck |
| 2010 | CAV | Lazy Annotation for Program Testing and Verification. | Kenneth L. McMillan |
| 2009 | CAV | Generalizing DPLL to Richer Logics. | Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv |
| 2009 | FMICS | What's in Common between Test, Model Checking, and Decision Procedures? | Kenneth L. McMillan |
| 2008 | POPL | Relevance heuristics for program analysis. | Kenneth L. McMillan |
| 2008 | TACAS | Quantified Invariant Generation Using an Interpolating Saturation Prover. | Kenneth L. McMillan |
| 2007 | ATVA | Toward Property-Driven Abstraction for Heap Manipulating Programs. | Kenneth L. McMillan |
| 2007 | CAV | Automated Assumption Generation for Compositional Verification. | Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu |
| 2007 | CAV | Array Abstractions from Proofs. | Ranjit Jhala, Kenneth L. McMillan |
| 2007 | TACAS | Combining Abstraction Refinement and SAT-Based Model Checking. | Nina Amla, Kenneth L. McMillan |
| 2007 | VMCAI | Interpolants and Symbolic Model Checking. | Kenneth L. McMillan |
| 2006 | CAV | Lazy Abstraction with Interpolants. | Kenneth L. McMillan |
| 2006 | FORTE | Liveness by Invisible Invariants. | Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck |
| 2006 | TACAS | A Practical and Complete Approach to Predicate Refinement. | Ranjit Jhala, Kenneth L. McMillan |
| 2005 | CAV | Interpolant-Based Transition Relation Approximation. | Ranjit Jhala, Kenneth L. McMillan |
| 2005 | TACAS | Applications of Craig Interpolants in Model Checking. | Kenneth L. McMillan |
| 2004 | CSL | Applications of Craig Interpolation to Model Checking. | Kenneth L. McMillan |
| 2004 | FMCAD | A Hybrid of Counterexample-Based and Proof-Based Abstraction. | Nina Amla, Kenneth L. McMillan |
| 2004 | POPL | Abstractions from proofs. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan |
| 2004 | TACAS | An Interpolating Theorem Prover. | Kenneth L. McMillan |
| 2003 | CAV | Interpolation and SAT-Based Model Checking. | Kenneth L. McMillan |
| 2003 | MEMOCODE | Methods for exploiting SAT solvers in unbounded model checking. | Kenneth L. McMillan |
| 2003 | SAS | Craig Interpolation and Reachability Analysis. | Kenneth L. McMillan |
| 2003 | TACAS | Experimental Analysis of Different Techniques for Bounded Model Checking. | Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo H. Medel |
| 2003 | TACAS | Automatic Abstraction without Counterexamples. | Kenneth L. McMillan, Nina Amla |
| 2002 | CAV | Applying SAT Methods in Unbounded Symbolic Model Checking. | Kenneth L. McMillan |
| 2001 | CAV | Microarchitecture Verification by Compositional Model Checking. | Ranjit Jhala, Kenneth L. McMillan |
| 2000 | CAV | Induction in Compositional Model Checking. | Kenneth L. McMillan, Shaz Qadeer, James B. Saxe |
| 2000 | LICS | Some Strategies for Proving Theorems with a Model Checker. | Kenneth L. McMillan |
| 1999 | CAV | Latency Insensitive Protocols. | Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli |
| 1999 | ICCAD | A methodology for correct-by-construction latency insensitive design. | Luca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli |
| 1999 | ICCAD | Probabilistic state space search. | Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton |
| 1998 | CAV | Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. | Kenneth L. McMillan |
| 1998 | DAC | Approximation and Decomposition of Binary Decision Diagrams. | Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi |
| 1998 | FMCAD | Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract). | Kenneth L. McMillan |
| 1998 | ICALP | Deciding Global Partial-Order Properties. | Rajeev Alur, Kenneth L. McMillan, Doron A. Peled |
| 1997 | CAV | A Compositional Rule for Hardware Design Refinement. | Kenneth L. McMillan |
| 1997 | DAC | Safe BDD Minimization Using Don't Cares. | Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan |
| 1996 | CAV | Symbolic Model Checking. | Edmund M. Clarke, Kenneth L. McMillan, Srgio Vale Aguiar Campos, Vasiliki Hartonas-Garmhausen |
| 1996 | CAV | A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. | Kenneth L. McMillan |
| 1996 | DAC | Engineering Change in a Non-Deterministic FSM Setting. | Sunil P. Khatri, Amit Narayan, Sriram C. Krishnan, Kenneth L. McMillan, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli |
| 1996 | LICS | Model-Checking of Correctness Conditions for Concurrent Objects. | Rajeev Alur, Kenneth L. McMillan, Doron A. Peled |
| 1995 | CAV | Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study. | sgeir Th. Eirksson, Kenneth L. McMillan |
| 1995 | CAV | Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. | Kenneth L. McMillan |
| 1995 | DAC | Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. | Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao |
| 1995 | ICCAD | Fast discrete function evaluation using decision diagrams. | Patrick C. McGeer, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli, Patrick Scaglia |
| 1994 | CAV | Hierarchical Representations of Discrete Functions, with Application to Model Checking. | Kenneth L. McMillan |
| 1994 | DAC | Panel: Complex System Verification: The Challenge Ahead. | Ronald Collett, Mike Gianfagna, Michel Courtoy, Martin Baynes, Johan Van Ginderdeuren, Kenneth L. McMillan, Stephen Ricca, Alberto L. Sangiovanni-Vincentelli, Steve Sapiro, Naeem Zafar |
| 1994 | DAC | Fitting Formal Methods into the Design Cycle. | Kenneth L. McMillan |
| 1993 | DAC | Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. | Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, Jerry Chih-Yuan Yang |
| 1992 | CAV | Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. | Kenneth L. McMillan |
| 1992 | ICCD | Algorithms for Interface Timing Verification. | Kenneth L. McMillan, David L. Dill |
| 1991 | ICCD | Synthesizing Converters Between Finite State Protocols. | Janaki Akella, Kenneth L. McMillan |
| 1990 | DAC | Sequential Circuit Verification Using Symbolic Model Checking. | Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill |
| 1990 | LICS | Symbolic Model Checking: 10^20 States and Beyond | Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang |
| 1989 | LICS | Compositional Model Checking | Edmund M. Clarke, David E. Long, Kenneth L. McMillan |
| 1989 | PODC | A Structural Induction Theorem for Processes. | Robert P. Kurshan, Kenneth L. McMillan |