Selected Publications
| 2006 | ||
|---|---|---|
| BibTeX | Ranjit Jhala, Kenneth L. McMillan: Lazy Abstraction with Interpolants. CAV 2006: 123-136 | |
| BibTeX | Ranjit Jhala, Kenneth L. McMillan: A Practical and Complete Approach to Predicate Refinement. TACAS 2006: 459-473 | |
| 2005 | ||
| BibTeX | Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. CAV 2005: 39-51 | |
| BibTeX | Nina 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 | |
| BibTeX | Kenneth L. McMillan: Applications of Craig Interpolants in Model Checking. TACAS 2005: 1-12 | |
| BibTeX | Rajeev Alur, Kenneth L. McMillan, Doron Peled: Deciding Global Partial-Order Properties. Formal Methods in System Design 26(1): 7-25 (2005) | |
| BibTeX | Kenneth L. McMillan: An interpolating theorem prover. Theor. Comput. Sci. 345(1): 101-121 (2005) | |
| 2004 | ||
| BibTeX | Nina Amla, Kenneth L. McMillan: A Hybrid of Counterexample-Based and Proof-Based Abstraction. FMCAD 2004: 260-274 | |
| BibTeX | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan: Abstractions from proofs. POPL 2004: 232-244 | |
| BibTeX | Kenneth L. McMillan: An Interpolating Theorem Prover. TACAS 2004: 16-30 | |
| 2003 | ||
| BibTeX | Kenneth L. McMillan: Interpolation and SAT-Based Model Checking. CAV 2003: 1-13 | |
| BibTeX | Kenneth L. McMillan, Nina Amla: Automatic Abstraction without Counterexamples. TACAS 2003: 2-17 | |
| BibTeX | Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo Medel: Experimental Analysis of Different Techniques for Bounded Model Checking. TACAS 2003: 34-48 | |
| BibTeX | Kenneth L. McMillan: Methods for exploiting SAT solvers in unbounded model checking. MEMOCODE 2003: 135-142 | |
| 2002 | ||
| BibTeX | Kenneth L. McMillan: Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002: 250-264 | |
| 2001 | ||
| BibTeX | Ranjit Jhala, Kenneth L. McMillan: Microarchitecture Verification by Compositional Model Checking. CAV 2001: 396-410 | |
| BibTeX | Kenneth L. McMillan: Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. CHARME 2001: 179-195 | |
| BibTeX | Luca 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 | |
| BibTeX | Youpyo 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 | ||
| BibTeX | Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli: Latency Insensitive Protocols. CAV 1999: 123-133 | |
| BibTeX | Kenneth L. McMillan: Verification of Infinite State Systems by Compositional Model Checking. CHARME 1999: 219-234 | |
| BibTeX | Kenneth L. McMillan: Circular Compositional Reasoning about Liveness. CHARME 1999: 342-345 | |
| BibTeX | Luca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli: A methodology for correct-by-construction latency insensitive design. ICCAD 1999: 309-315 | |
| BibTeX | Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton: Probabilistic state space search. ICCAD 1999: 574-579 | |
| 1998 | ||
| BibTeX | Kenneth L. McMillan: Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. CAV 1998: 110-121 | |
| BibTeX | Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi: Approximation and Decomposition of Binary Decision Diagrams. DAC 1998: 445-450 | |
| BibTeX | Rajeev Alur, Kenneth L. McMillan, Doron Peled: Deciding Global Partial-Order Properties. ICALP 1998: 41-52 | |
| 1997 | ||
| BibTeX | Kenneth L. McMillan: A Compositional Rule for Hardware Design Refinement. CAV 1997: 24-35 | |
| BibTeX | Youpyo 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) | |
| W.N.N. Hung, A. Aziz, K.L. McMillan: Heuristic symmetry reduction for invariant verification. IWLS 1997: | ||
| 1996 | ||
| BibTeX | Kenneth L. McMillan: A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. CAV 1996: 13-25 | |
| BibTeX | Sunil 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 | |
| BibTeX | Rajeev Alur, Kenneth L. McMillan, Doron Peled: Model-Checking of Correctness Conditions for Concurrent Objects. LICS 1996: 219-228 | |
| 1995 | ||
| BibTeX | Kenneth L. McMillan: Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. CAV 1995: 180-195 | |
| BibTeX | Á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 | |
| BibTeX | Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao: Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC 1995: 427-432 | |
| BibTeX | Kenneth 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 | ||
| BibTeX | Kenneth L. McMillan: Hierarchical Representations of Discrete Functions, with Application to Model Checking. CAV 1994: 41-54 | |
| BibTeX | Kenneth L. McMillan: Fitting Formal Methods into the Design Cycle. DAC 1994: 314-319 | |
| J. 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 | ||
| 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. CHDL 1993: 15-30 | |
| BibTeX | Edmund 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 | |
| BibTeX | Kenneth L. McMillan, David L. Dill: Algorithms for Interface Timing Verification. ICCD 1992: 48-51 | |
| BibTeX | Jerry 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) | ||
| K. L. McMillan: Symbolic Model Checking: an approach to the state explosion problem.CMU Tech Rpt. CMU-CS-92-131 | ||
| 1991 | ||
| BibTeX | Janaki Akella, Kenneth L. McMillan: Synthesizing Converters Between Finite State Protocols. ICCD 1991: 410-413 | |
| R. Kurshan, K. L. McMillan: Analysis of Digital Circuits through Symbolic Reduction. IEEE Trans. Computer-Aided Des. Integr. Circuits Syst. 10(11): 1356-71 (1991) | ||
| E. 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) | ||
| K. L. McMillan, J. Schwalbe: Formal verification of the Encore Gigamax cache consistency protocols. Internatinoal Symposium on Shared Memory Multiprocessors 1991: 242-51 | ||
| 1990 | ||
| BibTeX | Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill: Sequential Circuit Verification Using Symbolic Model Checking. DAC 1990: 46-51 | |
| BibTeX | Jerry 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 | ||
| BibTeX | Edmund M. Clarke, David E. Long, Kenneth L. McMillan: Compositional Model Checking LICS 1989: 353-362 | |
| BibTeX | Robert P. Kurshan, Kenneth L. McMillan: A Structural Induction Theorem for Processes. PODC 1989: 239-247 | |
| Edmund 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) | ||