Kenneth L. McMillan

2008
76	EE	Kenneth L. McMillan: Relevance heuristics for program analysis. POPL 2008: 145-146
75	EE	Kenneth L. McMillan: Quantified Invariant Generation Using an Interpolating Saturation Prover. TACAS 2008: 413-427
74	EE	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	EE	Kenneth L. McMillan: Toward Property-Driven Abstraction for Heap Manipulating Programs. ATVA 2007: 17-18
72	EE	Ranjit Jhala, Kenneth L. McMillan: Array Abstractions from Proofs. CAV 2007: 193-206
71	EE	Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu: Automated Assumption Generation for Compositional Verification. CAV 2007: 420-432
70	EE	Nina Amla, Kenneth L. McMillan: Combining Abstraction Refinement and SAT-Based Model Checking. TACAS 2007: 405-419
69	EE	Kenneth L. McMillan: Interpolants and Symbolic Model Checking. VMCAI 2007: 89-90
68	EE	Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation CoRR abs/0706.0523: (2007)
67	EE	Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. Logical Methods in Computer Science 3(4): (2007)
2006
66	EE	Kenneth L. McMillan: Lazy Abstraction with Interpolants. CAV 2006: 123-136
65	EE	Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck: Liveness by Invisible Invariants. FORTE 2006: 356-371
64	EE	Ranjit Jhala, Kenneth L. McMillan: A Practical and Complete Approach to Predicate Refinement. TACAS 2006: 459-473
2005
63	EE	Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. CAV 2005: 39-51
62	EE	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	EE	Kenneth L. McMillan: Applications of Craig Interpolation to Model Checking. ICATPN 2005: 15-16
60	EE	Kenneth L. McMillan: Applications of Craig Interpolants in Model Checking. TACAS 2005: 1-12
59	EE	Rajeev Alur, Kenneth L. McMillan, Doron Peled: Deciding Global Partial-Order Properties. Formal Methods in System Design 26(1): 7-25 (2005)
58	EE	Kenneth L. McMillan: An interpolating theorem prover. Theor. Comput. Sci. 345(1): 101-121 (2005)
2004
57	EE	Kenneth L. McMillan: Applications of Craig Interpolation to Model Checking. CSL 2004: 22-23
56	EE	Nina Amla, Kenneth L. McMillan: A Hybrid of Counterexample-Based and Proof-Based Abstraction. FMCAD 2004: 260-274
55	EE	Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan: Abstractions from proofs. POPL 2004: 232-244
54	EE	Kenneth L. McMillan: An Interpolating Theorem Prover. TACAS 2004: 16-30
2003
53	EE	Kenneth L. McMillan: Interpolation and SAT-Based Model Checking. CAV 2003: 1-13
52	EE	Kenneth L. McMillan: Methods for exploiting SAT solvers in unbounded model checking. MEMOCODE 2003: 135-
51	EE	Kenneth L. McMillan: Craig Interpolation and Reachability Analysis. SAS 2003: 336
50	EE	Kenneth L. McMillan, Nina Amla: Automatic Abstraction without Counterexamples. TACAS 2003: 2-17
49	EE	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	EE	Kenneth L. McMillan: Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002: 250-264
2001
47	EE	Ranjit Jhala, Kenneth L. McMillan: Microarchitecture Verification by Compositional Model Checking. CAV 2001: 396-410
46	EE	Kenneth L. McMillan: Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. CHARME 2001: 179-195
45	EE	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	EE	Kenneth L. McMillan: Some Strategies for Proving Theorems with a Model Checker. LICS 2000: 305-306
42	EE	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	EE	Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli: Latency Insensitive Protocols. CAV 1999: 123-133
38	EE	Kenneth L. McMillan: Verification of Infinite State Systems by Compositional Model Checking. CHARME 1999: 219-234
37	EE	Kenneth L. McMillan: Circular Compositional Reasoning about Liveness. CHARME 1999: 342-345
36	EE	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	EE	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	EE	Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi: Approximation and Decomposition of Binary Decision Diagrams. DAC 1998: 445-450
32	EE	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	EE	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	EE	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	EE	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	EE	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	EE	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	EE	Kenneth L. McMillan: Fitting Formal Methods into the Design Cycle. DAC 1994: 314-319
13	EE	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	EE	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	EE	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	EE	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	EE	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]
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	Alexander Saldanha	[19] [36]
46	Alberto L. Sangiovanni-Vincentelli	[13] [19] [24] [36] [39] [45]
47	Steve Sapiro	[13]
48	James B. Saxe	[44]
49	Patrick Scaglia	[19]
50	Thomas R. Shiple	[33]
51	Fabio Somenzi	[33]
52	J. Yang	[10] [27]
53	Naeem Zafar	[13]
54	Xudong Zhao	[10] [20] [27]
55	Lenore D. Zuck	[65]

Colors in the list of coauthors