Selected Publications


2010
BibTeX PDF Kenneth L. McMillan: Lazy Annotation for Program Testing and Verification. CAV 2010: 104-118
2009
BibTeX PDF Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv: Generalizing DPLL to Richer Logics. CAV 2009: 462-476
BibTeX PDF Kenneth L. McMillan, Lenore D. Zuck: Abstract Counterexamples for Non-disjunctive Abstractions. RP 2009: 176-188
2008
BibTeX PDF Kenneth L. McMillan: Quantified Invariant Generation Using an Interpolating Saturation Prover. TACAS 2008: 413-427
BibTeX PDF Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu: Automated assumption generation for compositional verification. Formal Methods in System Design 32(3): 285-301 (2008)
2007
BibTeX PDF Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu: Automated Assumption Generation for Compositional Verification. CAV 2007: 420-432
BibTeX PDF Nina Amla, Kenneth L. McMillan: Combining Abstraction Refinement and SAT-Based Model Checking. TACAS 2007: 405-419
BibTeX PDF Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. Logical Methods in Computer Science 3(4): (2007)
2006
BibTeXPDFRanjit Jhala, Kenneth L. McMillan: Lazy Abstraction with Interpolants. CAV 2006: 123-136
BibTeXPDFRanjit Jhala, Kenneth L. McMillan: A Practical and Complete Approach to Predicate Refinement. TACAS 2006: 459-473
BibTeX Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck: Liveness by Invisible Invariants. FORTE 2006: 356-371
2005
BibTeXPDFRanjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. CAV 2005: 39-51
BibTeXPDFNina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, Kenneth L. McMillan: An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment. CHARME 2005: 254-268
BibTeXPDFKenneth L. McMillan: Applications of Craig Interpolants in Model Checking. TACAS 2005: 1-12
BibTeXRajeev Alur, Kenneth L. McMillan, Doron Peled: Deciding Global Partial-Order Properties. Formal Methods in System Design 26(1): 7-25 (2005)
BibTeXPDFKenneth L. McMillan: An interpolating theorem prover. Theor. Comput. Sci. 345(1): 101-121 (2005)
2004
BibTeXNina Amla, Kenneth L. McMillan: A Hybrid of Counterexample-Based and Proof-Based Abstraction. FMCAD 2004: 260-274
BibTeXPDFThomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan: Abstractions from proofs. POPL 2004: 232-244
BibTeXPDFKenneth L. McMillan: An Interpolating Theorem Prover. TACAS 2004: 16-30
2003
BibTeXPDFKenneth L. McMillan: Interpolation and SAT-Based Model Checking. CAV 2003: 1-13
BibTeXPDFKenneth L. McMillan, Nina Amla: Automatic Abstraction without Counterexamples. TACAS 2003: 2-17
BibTeXPDFNina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo Medel: Experimental Analysis of Different Techniques for Bounded Model Checking. TACAS 2003: 34-48
BibTeXPDFKenneth L. McMillan: Methods for exploiting SAT solvers in unbounded model checking. MEMOCODE 2003: 135-142
2002
BibTeXPDFKenneth L. McMillan: Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002: 250-264
2001
BibTeXPDFRanjit Jhala, Kenneth L. McMillan: Microarchitecture Verification by Compositional Model Checking. CAV 2001: 396-410
BibTeXPDFKenneth L. McMillan: Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. CHARME 2001: 179-195
BibTeXLuca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli: Theory of latency-insensitive design. IEEE Trans. on CAD of Integrated Circuits and Systems 20(9): 1059-1076 (2001)
2000
BibTeX Kenneth L. McMillan, Shaz Qadeer, James B. Saxe: Induction in Compositional Model Checking. CAV 2000: 312-327
BibTeXPDFYoupyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan: Sibling-substitution-based BDD minimization using don't cares. IEEE Trans. on CAD of Integrated Circuits and Systems 19(1): 44-55 (2000)
BibTex Rajeev Alur, Kenneth L. McMillan, Doron Peled: Model-Checking of Correctness Conditions for Concurrent Objects. Inf. Comput. 160(1-2): 167-188 (2000)
BibTeX Kenneth L. McMillan: A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37(1-3): 279-309 (2000)
1999
BibTeXPDFLuca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli: Latency Insensitive Protocols. CAV 1999: 123-133
BibTeXPDFKenneth L. McMillan: Verification of Infinite State Systems by Compositional Model Checking. CHARME 1999: 219-234
BibTeXPDFKenneth L. McMillan: Circular Compositional Reasoning about Liveness. CHARME 1999: 342-345
BibTeXPDFLuca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli: A methodology for correct-by-construction latency insensitive design. ICCAD 1999: 309-315
BibTeXPDFAndreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton: Probabilistic state space search. ICCAD 1999: 574-579
1998
BibTeXPDFKenneth L. McMillan: Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. CAV 1998: 110-121
BibTeXPDFKavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi: Approximation and Decomposition of Binary Decision Diagrams. DAC 1998: 445-450
BibTeXPDFRajeev Alur, Kenneth L. McMillan, Doron Peled: Deciding Global Partial-Order Properties. ICALP 1998: 41-52
1997
BibTeXPDFKenneth L. McMillan: A Compositional Rule for Hardware Design Refinement. CAV 1997: 24-35
BibTeXPDFYoupyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan: Safe BDD Minimization Using Don't Cares. DAC 1997: 208-213
BibTeX Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, J. Yang: Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. Formal Methods in System Design 10(2/3): 137-148 (1997)
 PDFW.N.N. Hung, A. Aziz, K.L. McMillan: Heuristic symmetry reduction for invariant verification. IWLS 1997:
1996
BibTeXPDFKenneth L. McMillan: A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. CAV 1996: 13-25
BibTeXPDFSunil P. Khatri, Amit Narayan, Sriram C. Krishnan, Kenneth L. McMillan, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli: Engineering Change in a Non-Deterministic FSM Setting. DAC 1996: 451-456
BibTeXPDFRajeev Alur, Kenneth L. McMillan, Doron Peled: Model-Checking of Correctness Conditions for Concurrent Objects. LICS 1996: 219-228
1995
BibTeXPDFKenneth L. McMillan: Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. CAV 1995: 180-195
BibTeXPDFÁsgeir Th. Eiríksson, Kenneth L. McMillan: Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study. CAV 1995: 367-380
BibTeXPDFEdmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao: Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC 1995: 427-432
BibTeXPDFKenneth L. McMillan: A Technique of State Space Search Based on Unfolding. Formal Methods in System Design 6(1): 45-65 (1995)
BibTeX Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness: Verification of the Futurebus+ Cache Coherence Protocol. Formal Methods in System Design 6(2): 217-232 (1995)
BibTeX Robert P. Kurshan, Kenneth L. McMillan: A Structural Induction Theorem for Processes Inf. Comput. 117(1): 1-11 (1995)
1994
BibTeXPDFKenneth L. McMillan: Hierarchical Representations of Discrete Functions, with Application to Model Checking. CAV 1994: 41-54
BibTeXPDFKenneth L. McMillan: Fitting Formal Methods into the Design Cycle. DAC 1994: 314-319
 PDFJ. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, D. L. Dill: Symbolic Model Checking for Sequential Circuit Verification. IEEE Trans. on CAD of Integrated Circuits and Systems 13(4): 401-24 (1994)
1993
BibTeXPDFEdmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness: Verification of the Futurebus+ Cache Coherence Protocol. CHDL 1993: 15-30
BibTeXPDFEdmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, J. Yang: Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. DAC 1993: 54-60
  K. L. McMillan: Symbolic Model Checking. Kluwer Academic Publishers, 1993
1992
BibTeX Kenneth L. McMillan: Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. CAV 1992: 164-177
BibTeXPDFKenneth L. McMillan, David L. Dill: Algorithms for Interface Timing Verification. ICCD 1992: 48-51
BibTeXPDFJerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang: Symbolic Model Checking: 10^20 States and Beyond Inf. Comput. 98(2): 142-170 (1992)
  E. M. Clarke, J. R. Burch, O. Grumberg, D. E. Long, K. L. McMillan: Automatic verification of sequential circuit designs. Philosophical Transactions of the Royal Society, Series A, 339: 105-20 (1992)
 PDFK. L. McMillan: Symbolic Model Checking: an approach to the state explosion problem.CMU Tech Rpt. CMU-CS-92-131
1991
BibTeXPDFJanaki Akella, Kenneth L. McMillan: Synthesizing Converters Between Finite State Protocols. ICCD 1991: 410-413
 PDFR. Kurshan, K. L. McMillan: Analysis of Digital Circuits through Symbolic Reduction. IEEE Trans. Computer-Aided Des. Integr. Circuits Syst. 10(11): 1356-71 (1991)
 PDFE. M. Clarke, D. E. Long, K. L. McMillan: A language for compositional specification and verification of finite state hardware controllers. Proceedings of the IEEE. 79(9): 1283-92 (1991)
 PDF K. L. McMillan, J. Schwalbe: Formal verification of the Encore Gigamax cache consistency protocols. Internatinoal Symposium on Shared Memory Multiprocessors 1991: 242-51
1990
BibTeXPDFJerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill: Sequential Circuit Verification Using Symbolic Model Checking. DAC 1990: 46-51
BibTeXPDFJerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang: Symbolic Model Checking: 10^20 States and Beyond LICS 1990: 428-439
1989
BibTeXPDFEdmund M. Clarke, David E. Long, Kenneth L. McMillan: Compositional Model Checking LICS 1989: 353-362
BibTeXPDFRobert P. Kurshan, Kenneth L. McMillan: A Structural Induction Theorem for Processes. PODC 1989: 239-247
 PDFEdmund M. Clarke, David E. Long, and K.L. Mcmillan: A language for compositional specification and verification of finite state hardware controllers. CHDL 1989: 1283-1292
1986
  K.C. McGill, K.L. McMillan: A Smart Trigger for real-time spike classification. Proceedings of the Eighth Annual Conference of the IEEE/Engineering in Medicine and Biology Society, vol. 1: 275-8 (1986)
  R. Steele, D. Hennies, J. Duluk, E. Vogel, K. McMillan: Software modules for a hand-scanned reading aid for the blind. Proceedings of the Ninth Annual Conference on Rehabilitation Technology: 43-5 (1986)