Kenneth L. McMillan

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

Colors in the list of coauthors

Last update Sun Jun 3 16:06:10 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page