Please note: This is a beta version of the new dblp website.
You can find the classic dblp view of this page here.
You can find the classic dblp view of this page here.
Kenneth L. McMillan
2010 – today
- 2013
[c72]Nikolaj Bjørner, Kenneth L. McMillan, Andrey Rybalchenko: On Solving Universally Quantified Horn Clauses. SAS 2013: 105-125- [c71]Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv: Synthesis of Circular Compositional Program Proofs via Abduction. TACAS 2013: 370-384
- 2012
- [c70]Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken: Minimum Satisfying Assignments for SMT. CAV 2012: 394-409
- [c69]Thomas Ball, Nikolaj Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes: Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. SPIN 2012: 1-6
- 2011
- [c68]
- [c67]
- [c66]Kenneth L. McMillan, Lenore D. Zuck: Invisible Invariants and Abstract Interpretation. SAS 2011: 249-262
- 2010
- [c65]
2000 – 2009
- 2009
- [c64]Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv: Generalizing DPLL to Richer Logics. CAV 2009: 462-476
- [c63]Kenneth L. McMillan: What's in Common between Test, Model Checking, and Decision Procedures? FMICS 2009: 35-36
- [c62]Kenneth L. McMillan, Lenore D. Zuck: Abstract Counterexamples for Non-disjunctive Abstractions. RP 2009: 176-188
- 2008
- [j15]Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu: Automated assumption generation for compositional verification. Formal Methods in System Design 32(3): 285-301 (2008)
- [c61]Kenneth L. McMillan: Proofs, Interpolants, and Relevance Heuristics. Haifa Verification Conference 2008: 3
- [c60]
- [c59]Kenneth L. McMillan: Quantified Invariant Generation Using an Interpolating Saturation Prover. TACAS 2008: 413-427
- 2007
- [j14]Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. Logical Methods in Computer Science 3(4) (2007)
- [c58]Kenneth L. McMillan: Toward Property-Driven Abstraction for Heap Manipulating Programs. ATVA 2007: 17-18
- [c57]
- [c56]Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu: Automated Assumption Generation for Compositional Verification. CAV 2007: 420-432
- [c55]Nina Amla, Kenneth L. McMillan: Combining Abstraction Refinement and SAT-Based Model Checking. TACAS 2007: 405-419
- [c54]
- [i1]Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. CoRR abs/0706.0523 (2007)
- 2006
- [c53]
- [c52]Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck: Liveness by Invisible Invariants. FORTE 2006: 356-371
- [c51]Ranjit Jhala, Kenneth L. McMillan: A Practical and Complete Approach to Predicate Refinement. TACAS 2006: 459-473
- 2005
- [j13]Rajeev Alur, Kenneth L. McMillan, Doron Peled: Deciding Global Partial-Order Properties. Formal Methods in System Design 26(1): 7-25 (2005)
- [j12]
- [c50]
- [c49]Ranjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. CAV 2005: 39-51
- [c48]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
- [c47]
- 2004
- [c46]
- [c45]Nina Amla, Kenneth L. McMillan: A Hybrid of Counterexample-Based and Proof-Based Abstraction. FMCAD 2004: 260-274
- [c44]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan: Abstractions from proofs. POPL 2004: 232-244
- [c43]
- 2003
- [c42]
- [c41]Kenneth L. McMillan: Methods for exploiting SAT solvers in unbounded model checking. MEMOCODE 2003: 135-
- [c40]
- [c39]
- [c38]Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo Medel: Experimental Analysis of Different Techniques for Bounded Model Checking. TACAS 2003: 34-48
- 2002
- [c37]
- 2001
- [j11]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)
- [c36]Ranjit Jhala, Kenneth L. McMillan: Microarchitecture Verification by Compositional Model Checking. CAV 2001: 396-410
- [c35]Kenneth L. McMillan: Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. CHARME 2001: 179-195
- 2000
- [j10]Rajeev Alur, Kenneth L. McMillan, Doron Peled: Model-Checking of Correctness Conditions for Concurrent Objects. Inf. Comput. 160(1-2): 167-188 (2000)
- [j9]Kenneth L. McMillan: A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37(1-3): 279-309 (2000)
- [j8]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)
- [c34]Kenneth L. McMillan, Shaz Qadeer, James B. Saxe: Induction in Compositional Model Checking. CAV 2000: 312-327
- [c33]
1990 – 1999
- 1999
- [c32]Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli: Latency Insensitive Protocols. CAV 1999: 123-133
- [c31]Kenneth L. McMillan: Verification of Infinite State Systems by Compositional Model Checking. CHARME 1999: 219-234
- [c30]
- [c29]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
- [c28]Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton: Probabilistic state space search. ICCAD 1999: 574-579
- 1998
- [c27]Kenneth L. McMillan: Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. CAV 1998: 110-121
- [c26]Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi: Approximation and Decomposition of Binary Decision Diagrams. DAC 1998: 445-450
- [c25]Kenneth L. McMillan: Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract). FMCAD 1998: 1
- [c24]
- [c23]Rajeev Alur, Kenneth L. McMillan, Doron Peled: Deciding Global Partial-Order Properties. ICALP 1998: 41-52
- 1997
- [j7]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)
- [c22]
- [c21]Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan: Safe BDD Minimization Using Don't Cares. DAC 1997: 208-213
- 1996
- [c20]Kenneth L. McMillan: A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. CAV 1996: 13-25
- [c19]Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vassili Hartonas-Garmhausen: Symbolic Model Checking. CAV 1996: 419-427
- [c18]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
- [c17]Rajeev Alur, Kenneth L. McMillan, Doron Peled: Model-Checking of Correctness Conditions for Concurrent Objects. LICS 1996: 219-228
- 1995
- [j6]Kenneth L. McMillan: A Technique of State Space Search Based on Unfolding. Formal Methods in System Design 6(1): 45-65 (1995)
- [j5]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)
- [j4]Robert P. Kurshan, Kenneth L. McMillan: A Structural Induction Theorem for Processes. Inf. Comput. 117(1): 1-11 (1995)
- [c16]Kenneth L. McMillan: Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. CAV 1995: 180-195
- [c15]Á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
- [c14]Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao: Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC 1995: 427-432
- [c13]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
- 1994
- [j3]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)
- [c12]Kenneth L. McMillan: Hierarchical Representations of Discrete Functions, with Application to Model Checking. CAV 1994: 41-54
- [c11]
- [c10]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
- 1993
- [b1]Kenneth L. McMillan: Symbolic model checking. Kluwer 1993, ISBN 978-0-7923-9380-1, pp. I-XV, 1-194
- [c9]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
- [c8]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
- [j2]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)
- [c7]Kenneth L. McMillan: Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. CAV 1992: 164-177
- [c6]
- 1991
- [j1]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)
- [c5]Janaki Akella, Kenneth L. McMillan: Synthesizing Converters Between Finite State Protocols. ICCD 1991: 410-413
- 1990
- [c4]Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill: Sequential Circuit Verification Using Symbolic Model Checking. DAC 1990: 46-51
- [c3]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
1980 – 1989
- 1989
- [c2]Edmund M. Clarke, David E. Long, Kenneth L. McMillan: Compositional Model Checking. LICS 1989: 353-362
- [c1]Robert P. Kurshan, Kenneth L. McMillan: A Structural Induction Theorem for Processes. PODC 1989: 239-247
Coauthor Index
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-18 22:44 CEST by the dblp team