Kenneth L. McMillan

	2009
80		Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv: Generalizing DPLL to Richer Logics. CAV 2009: 462-476
79		Kenneth L. McMillan: What's in Common between Test, Model Checking, and Decision Procedures? FMICS 2009: 35-36
78		Kenneth L. McMillan, Lenore D. Zuck: Abstract Counterexamples for Non-disjunctive Abstractions. RP 2009: 176-188
	2008
77		Kenneth L. McMillan: Proofs, Interpolants, and Relevance Heuristics. Haifa Verification Conference 2008: 3
76		Kenneth L. McMillan: Relevance heuristics for program analysis. POPL 2008: 145-146
75		Kenneth L. McMillan: Quantified Invariant Generation Using an Interpolating Saturation Prover. TACAS 2008: 413-427
74		Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu: Automated assumption generation for compositional verification. Formal Methods in System Design 32(3): 285-301 (2008)
	2007
73		Kenneth L. McMillan: Toward Property-Driven Abstraction for Heap Manipulating Programs. ATVA 2007: 17-18
72		Ranjit Jhala, Kenneth L. McMillan: Array Abstractions from Proofs. CAV 2007: 193-206
71		Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu: Automated Assumption Generation for Compositional Verification. CAV 2007: 420-432
70		Nina Amla, Kenneth L. McMillan: Combining Abstraction Refinement and SAT-Based Model Checking. TACAS 2007: 405-419
69		Kenneth L. McMillan: Interpolants and Symbolic Model Checking. VMCAI 2007: 89-90
68		Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation CoRR abs/0706.0523: (2007)
67		Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. Logical Methods in Computer Science 3(4): (2007)
	2006
66		Kenneth L. McMillan: Lazy Abstraction with Interpolants. CAV 2006: 123-136
65		Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck: Liveness by Invisible Invariants. FORTE 2006: 356-371
64		Ranjit Jhala, Kenneth L. McMillan: A Practical and Complete Approach to Predicate Refinement. TACAS 2006: 459-473
	2005
63		Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. CAV 2005: 39-51
62		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
61		Kenneth L. McMillan: Applications of Craig Interpolation to Model Checking. ICATPN 2005: 15-16
60		Kenneth L. McMillan: Applications of Craig Interpolants in Model Checking. TACAS 2005: 1-12
59		Rajeev Alur, Kenneth L. McMillan, Doron Peled: Deciding Global Partial-Order Properties. Formal Methods in System Design 26(1): 7-25 (2005)
58		Kenneth L. McMillan: An interpolating theorem prover. Theor. Comput. Sci. 345(1): 101-121 (2005)
	2004
57		Kenneth L. McMillan: Applications of Craig Interpolation to Model Checking. CSL 2004: 22-23
56		Nina Amla, Kenneth L. McMillan: A Hybrid of Counterexample-Based and Proof-Based Abstraction. FMCAD 2004: 260-274
55		Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan: Abstractions from proofs. POPL 2004: 232-244
54		Kenneth L. McMillan: An Interpolating Theorem Prover. TACAS 2004: 16-30
	2003
53		Kenneth L. McMillan: Interpolation and SAT-Based Model Checking. CAV 2003: 1-13
52		Kenneth L. McMillan: Methods for exploiting SAT solvers in unbounded model checking. MEMOCODE 2003: 135-
51		Kenneth L. McMillan: Craig Interpolation and Reachability Analysis. SAS 2003: 336
50		Kenneth L. McMillan, Nina Amla: Automatic Abstraction without Counterexamples. TACAS 2003: 2-17
49		Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo Medel: Experimental Analysis of Different Techniques for Bounded Model Checking. TACAS 2003: 34-48
	2002
48		Kenneth L. McMillan: Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002: 250-264
	2001
47		Ranjit Jhala, Kenneth L. McMillan: Microarchitecture Verification by Compositional Model Checking. CAV 2001: 396-410
46		Kenneth L. McMillan: Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. CHARME 2001: 179-195
45		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
44		Kenneth L. McMillan, Shaz Qadeer, James B. Saxe: Induction in Compositional Model Checking. CAV 2000: 312-327
43		Kenneth L. McMillan: Some Strategies for Proving Theorems with a Model Checker. LICS 2000: 305-306
42		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)
41		Rajeev Alur, Kenneth L. McMillan, Doron Peled: Model-Checking of Correctness Conditions for Concurrent Objects. Inf. Comput. 160(1-2): 167-188 (2000)
40		Kenneth L. McMillan: A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37(1-3): 279-309 (2000)
	1999
39		Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli: Latency Insensitive Protocols. CAV 1999: 123-133
38		Kenneth L. McMillan: Verification of Infinite State Systems by Compositional Model Checking. CHARME 1999: 219-234
37		Kenneth L. McMillan: Circular Compositional Reasoning about Liveness. CHARME 1999: 342-345
36		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
35		Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton: Probabilistic state space search. ICCAD 1999: 574-579
	1998
34		Kenneth L. McMillan: Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. CAV 1998: 110-121
33		Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi: Approximation and Decomposition of Binary Decision Diagrams. DAC 1998: 445-450
32		Kenneth L. McMillan: Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract). FMCAD 1998: 1
31		Kenneth L. McMillan: Proof Rules for Model Checking Systems with Data. FSTTCS 1998: 270
30		Rajeev Alur, Kenneth L. McMillan, Doron Peled: Deciding Global Partial-Order Properties. ICALP 1998: 41-52
	1997
29		Kenneth L. McMillan: A Compositional Rule for Hardware Design Refinement. CAV 1997: 24-35
28		Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan: Safe BDD Minimization Using Don't Cares. DAC 1997: 208-213
27		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)
	1996
26		Kenneth L. McMillan: A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. CAV 1996: 13-25
25		Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vassili Hartonas-Garmhausen: Symbolic Model Checking. CAV 1996: 419-427
24		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
23		Rajeev Alur, Kenneth L. McMillan, Doron Peled: Model-Checking of Correctness Conditions for Concurrent Objects. LICS 1996: 219-228
	1995
22		Kenneth L. McMillan: Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. CAV 1995: 180-195
21		Á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
20		Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao: Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC 1995: 427-432
19		Patrick C. McGeer, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli, Patrick Scaglia: Fast discrete function evaluation using decision diagrams. ICCAD 1995: 402-407
18		Kenneth L. McMillan: A Technique of State Space Search Based on Unfolding. Formal Methods in System Design 6(1): 45-65 (1995)
17		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)
16		Robert P. Kurshan, Kenneth L. McMillan: A Structural Induction Theorem for Processes Inf. Comput. 117(1): 1-11 (1995)
	1994
15		Kenneth L. McMillan: Hierarchical Representations of Discrete Functions, with Application to Model Checking. CAV 1994: 41-54
14		Kenneth L. McMillan: Fitting Formal Methods into the Design Cycle. DAC 1994: 314-319
13		Ronald Collett, Mike Gianfagna, Michel Courtoy, Martin Baynes, Johan Van Ginderdeuren, Kenneth L. McMillan, Stephen Ricca, Alberto L. Sangiovanni-Vincentelli, Steve Sapiro, Naeem Zafar: Panel: Complex System Verification: The Challenge Ahead. DAC 1994: 320
12		Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, David L. Dill: Symbolic model checking for sequential circuit verification. IEEE Trans. on CAD of Integrated Circuits and Systems 13(4): 401-424 (1994)
	1993
11		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
10		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
	1992
9		Kenneth L. McMillan: Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. CAV 1992: 164-177
8		Kenneth L. McMillan, David L. Dill: Algorithms for Interface Timing Verification. ICCD 1992: 48-51
7		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)
	1991
6		Janaki Akella, Kenneth L. McMillan: Synthesizing Converters Between Finite State Protocols. ICCD 1991: 410-413
5		Robert P. Kurshan, Kenneth L. McMillan: Analysis of digital circuits through symbolic reduction. IEEE Trans. on CAD of Integrated Circuits and Systems 10(11): 1356-1371 (1991)
	1990
4		Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill: Sequential Circuit Verification Using Symbolic Model Checking. DAC 1990: 46-51
3		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
2		Edmund M. Clarke, David E. Long, Kenneth L. McMillan: Compositional Model Checking LICS 1989: 353-362
1		Robert P. Kurshan, Kenneth L. McMillan: A Structural Induction Theorem for Processes. PODC 1989: 239-247

Coauthor Index

1	Janaki Akella	[6]
2	Rajeev Alur	[23] [30] [41] [59]
3	Nina Amla	[49] [50] [56] [62] [70]
4	Martin Baynes	[13]
5	Peter A. Beerel	[28] [42]
6	Robert K. Brayton	[24] [35]
7	Jerry R. Burch	[3] [4] [7] [12] [28] [42]
8	Sérgio Vale Aguiar Campos	[25]
9	Luca P. Carloni	[36] [39] [45]
10	Edmund M. Clarke	[2] [3] [4] [7] [10] [11] [12] [17] [20] [25] [27]
11	Ronald Collett	[13]
12	Michel Courtoy	[13]
13	David L. Dill	[3] [4] [7] [8] [12]
14	Xiaoqun Du	[62]
15	Ásgeir Th. Eiríksson	[21]
16	Yi Fang	[65]
17	Zhaohui Fu	[71] [74]
18	Masahiro Fujita	[10] [27]
19	Mike Gianfagna	[13]
20	Johan Van Ginderdeuren	[13]
21	Orna Grumberg	[11] [17] [20]
22	Anubhav Gupta	[71] [74]
23	Vassili Hartonas-Garmhausen	[25]
24	Thomas A. Henzinger	[55]
25	Hiromi Hiraishi	[11] [17]
26	Youpyo Hong	[28] [42]
27	L. J. Hwang	[3] [7]
28	Somesh Jha	[11] [17]
29	Ranjit Jhala	[47] [55] [63] [64] [67] [68] [72]
30	Sunil P. Khatri	[24]
31	Sriram C. Krishnan	[24]
32	Andreas Kuehlmann	[35] [62] [80]
33	Robert P. Kurshan	[1] [5] [16] [49] [62]
34	David E. Long	[2] [11] [12] [17]
35	Rupak Majumdar	[55]
36	Patrick C. McGeer	[19]
37	Ricardo Medel	[49]
38	Amit Narayan	[24]
39	Linda A. Ness	[11] [17]
40	Doron Peled	[23] [30] [41] [59]
41	Amir Pnueli	[65]
42	Shaz Qadeer	[44]
43	Kavita Ravi	[33]
44	Stephen Ricca	[13]
45	Shmuel Sagiv (Mooly Sagiv)	[80]
46	Alexander Saldanha	[19] [36]
47	Alberto L. Sangiovanni-Vincentelli	[13] [19] [24] [36] [39] [45]
48	Steve Sapiro	[13]
49	James B. Saxe	[44]
50	Patrick Scaglia	[19]
51	Thomas R. Shiple	[33]
52	Fabio Somenzi	[33]
53	J. Yang	[10] [27]
54	Naeem Zafar	[13]
55	Xudong Zhao	[10] [20] [27]
56	Lenore D. Zuck	[65] [78]

Colors in the list of coauthors