The SCEAS System
Navigation Menu

Search the dblp DataBase

Title:
Author:

Kenneth L. McMillan: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang
    Symbolic Model Checking: 10^20 States and Beyond [Citation Graph (1, 0)][DBLP]
    Inf. Comput., 1992, v:98, n:2, pp:142-170 [Journal]
  2. Kenneth L. McMillan
    Applications of Craig Interpolation to Model Checking. [Citation Graph (0, 0)][DBLP]
    ICATPN, 2005, pp:15-16 [Conf]
  3. Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli
    Latency Insensitive Protocols. [Citation Graph (0, 0)][DBLP]
    CAV, 1999, pp:123-133 [Conf]
  4. Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vassili Hartonas-Garmhausen
    Symbolic Model Checking. [Citation Graph (0, 0)][DBLP]
    CAV, 1996, pp:419-427 [Conf]
  5. Ásgeir Th. Eiríksson, Kenneth L. McMillan
    Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study. [Citation Graph (0, 0)][DBLP]
    CAV, 1995, pp:367-380 [Conf]
  6. Ranjit Jhala, Kenneth L. McMillan
    Microarchitecture Verification by Compositional Model Checking. [Citation Graph (0, 0)][DBLP]
    CAV, 2001, pp:396-410 [Conf]
  7. Ranjit Jhala, Kenneth L. McMillan
    Interpolant-Based Transition Relation Approximation. [Citation Graph (0, 0)][DBLP]
    CAV, 2005, pp:39-51 [Conf]
  8. Kenneth L. McMillan
    Applying SAT Methods in Unbounded Symbolic Model Checking. [Citation Graph (0, 0)][DBLP]
    CAV, 2002, pp:250-264 [Conf]
  9. Kenneth L. McMillan
    Interpolation and SAT-Based Model Checking. [Citation Graph (0, 0)][DBLP]
    CAV, 2003, pp:1-13 [Conf]
  10. Kenneth L. McMillan
    Lazy Abstraction with Interpolants. [Citation Graph (0, 0)][DBLP]
    CAV, 2006, pp:123-136 [Conf]
  11. Kenneth L. McMillan
    Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. [Citation Graph (0, 0)][DBLP]
    CAV, 1992, pp:164-177 [Conf]
  12. Kenneth L. McMillan
    Hierarchical Representations of Discrete Functions, with Application to Model Checking. [Citation Graph (0, 0)][DBLP]
    CAV, 1994, pp:41-54 [Conf]
  13. Kenneth L. McMillan
    Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. [Citation Graph (0, 0)][DBLP]
    CAV, 1995, pp:180-195 [Conf]
  14. Kenneth L. McMillan
    A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. [Citation Graph (0, 0)][DBLP]
    CAV, 1996, pp:13-25 [Conf]
  15. Kenneth L. McMillan
    A Compositional Rule for Hardware Design Refinement. [Citation Graph (0, 0)][DBLP]
    CAV, 1997, pp:24-35 [Conf]
  16. Kenneth L. McMillan
    Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. [Citation Graph (0, 0)][DBLP]
    CAV, 1998, pp:110-121 [Conf]
  17. Kenneth L. McMillan, Shaz Qadeer, James B. Saxe
    Induction in Compositional Model Checking. [Citation Graph (0, 0)][DBLP]
    CAV, 2000, pp:312-327 [Conf]
  18. Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, Kenneth L. McMillan
    An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment. [Citation Graph (0, 0)][DBLP]
    CHARME, 2005, pp:254-268 [Conf]
  19. Kenneth L. McMillan
    Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. [Citation Graph (0, 0)][DBLP]
    CHARME, 2001, pp:179-195 [Conf]
  20. Kenneth L. McMillan
    Verification of Infinite State Systems by Compositional Model Checking. [Citation Graph (0, 0)][DBLP]
    CHARME, 1999, pp:219-234 [Conf]
  21. Kenneth L. McMillan
    Circular Compositional Reasoning about Liveness. [Citation Graph (0, 0)][DBLP]
    CHARME, 1999, pp:342-345 [Conf]
  22. 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. [Citation Graph (0, 0)][DBLP]
    CHDL, 1993, pp:15-30 [Conf]
  23. Kenneth L. McMillan
    Applications of Craig Interpolation to Model Checking. [Citation Graph (0, 0)][DBLP]
    CSL, 2004, pp:22-23 [Conf]
  24. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill
    Sequential Circuit Verification Using Symbolic Model Checking. [Citation Graph (0, 0)][DBLP]
    DAC, 1990, pp:46-51 [Conf]
  25. Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao
    Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. [Citation Graph (0, 0)][DBLP]
    DAC, 1995, pp:427-432 [Conf]
  26. Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, J. Yang
    Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. [Citation Graph (0, 0)][DBLP]
    DAC, 1993, pp:54-60 [Conf]
  27. 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. [Citation Graph (0, 0)][DBLP]
    DAC, 1994, pp:320- [Conf]
  28. Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan
    Safe BDD Minimization Using Don't Cares. [Citation Graph (0, 0)][DBLP]
    DAC, 1997, pp:208-213 [Conf]
  29. 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. [Citation Graph (0, 0)][DBLP]
    DAC, 1996, pp:451-456 [Conf]
  30. Kenneth L. McMillan
    Fitting Formal Methods into the Design Cycle. [Citation Graph (0, 0)][DBLP]
    DAC, 1994, pp:314-319 [Conf]
  31. Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi
    Approximation and Decomposition of Binary Decision Diagrams. [Citation Graph (0, 0)][DBLP]
    DAC, 1998, pp:445-450 [Conf]
  32. Nina Amla, Kenneth L. McMillan
    A Hybrid of Counterexample-Based and Proof-Based Abstraction. [Citation Graph (0, 0)][DBLP]
    FMCAD, 2004, pp:260-274 [Conf]
  33. Kenneth L. McMillan
    Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract). [Citation Graph (0, 0)][DBLP]
    FMCAD, 1998, pp:1- [Conf]
  34. Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck
    Liveness by Invisible Invariants. [Citation Graph (0, 0)][DBLP]
    FORTE, 2006, pp:356-371 [Conf]
  35. Kenneth L. McMillan
    Proof Rules for Model Checking Systems with Data. [Citation Graph (0, 0)][DBLP]
    FSTTCS, 1998, pp:270- [Conf]
  36. Rajeev Alur, Kenneth L. McMillan, Doron Peled
    Deciding Global Partial-Order Properties. [Citation Graph (0, 0)][DBLP]
    ICALP, 1998, pp:41-52 [Conf]
  37. Luca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli
    A methodology for correct-by-construction latency insensitive design. [Citation Graph (0, 0)][DBLP]
    ICCAD, 1999, pp:309-315 [Conf]
  38. Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton
    Probabilistic state space search. [Citation Graph (0, 0)][DBLP]
    ICCAD, 1999, pp:574-579 [Conf]
  39. Patrick C. McGeer, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli, Patrick Scaglia
    Fast discrete function evaluation using decision diagrams. [Citation Graph (0, 0)][DBLP]
    ICCAD, 1995, pp:402-407 [Conf]
  40. Janaki Akella, Kenneth L. McMillan
    Synthesizing Converters Between Finite State Protocols. [Citation Graph (0, 0)][DBLP]
    ICCD, 1991, pp:410-413 [Conf]
  41. Kenneth L. McMillan, David L. Dill
    Algorithms for Interface Timing Verification. [Citation Graph (0, 0)][DBLP]
    ICCD, 1992, pp:48-51 [Conf]
  42. Rajeev Alur, Kenneth L. McMillan, Doron Peled
    Model-Checking of Correctness Conditions for Concurrent Objects. [Citation Graph (0, 0)][DBLP]
    LICS, 1996, pp:219-228 [Conf]
  43. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang
    Symbolic Model Checking: 10^20 States and Beyond [Citation Graph (0, 0)][DBLP]
    LICS, 1990, pp:428-439 [Conf]
  44. Edmund M. Clarke, David E. Long, Kenneth L. McMillan
    Compositional Model Checking [Citation Graph (0, 0)][DBLP]
    LICS, 1989, pp:353-362 [Conf]
  45. Kenneth L. McMillan
    Some Strategies for Proving Theorems with a Model Checker. [Citation Graph (0, 0)][DBLP]
    LICS, 2000, pp:305-306 [Conf]
  46. Kenneth L. McMillan
    Methods for exploiting SAT solvers in unbounded model checking. [Citation Graph (0, 0)][DBLP]
    MEMOCODE, 2003, pp:135-0 [Conf]
  47. Robert P. Kurshan, Kenneth L. McMillan
    A Structural Induction Theorem for Processes. [Citation Graph (0, 0)][DBLP]
    PODC, 1989, pp:239-247 [Conf]
  48. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan
    Abstractions from proofs. [Citation Graph (0, 0)][DBLP]
    POPL, 2004, pp:232-244 [Conf]
  49. Kenneth L. McMillan
    Craig Interpolation and Reachability Analysis. [Citation Graph (0, 0)][DBLP]
    SAS, 2003, pp:336- [Conf]
  50. Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo Medel
    Experimental Analysis of Different Techniques for Bounded Model Checking. [Citation Graph (0, 0)][DBLP]
    TACAS, 2003, pp:34-48 [Conf]
  51. Ranjit Jhala, Kenneth L. McMillan
    A Practical and Complete Approach to Predicate Refinement. [Citation Graph (0, 0)][DBLP]
    TACAS, 2006, pp:459-473 [Conf]
  52. Kenneth L. McMillan
    An Interpolating Theorem Prover. [Citation Graph (0, 0)][DBLP]
    TACAS, 2004, pp:16-30 [Conf]
  53. Kenneth L. McMillan
    Applications of Craig Interpolants in Model Checking. [Citation Graph (0, 0)][DBLP]
    TACAS, 2005, pp:1-12 [Conf]
  54. Kenneth L. McMillan, Nina Amla
    Automatic Abstraction without Counterexamples. [Citation Graph (0, 0)][DBLP]
    TACAS, 2003, pp:2-17 [Conf]
  55. Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, J. Yang
    Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. [Citation Graph (0, 0)][DBLP]
    Formal Methods in System Design, 1997, v:10, n:2/3, pp:137-148 [Journal]
  56. Rajeev Alur, Kenneth L. McMillan, Doron Peled
    Deciding Global Partial-Order Properties. [Citation Graph (0, 0)][DBLP]
    Formal Methods in System Design, 2005, v:26, n:1, pp:7-25 [Journal]
  57. 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. [Citation Graph (0, 0)][DBLP]
    Formal Methods in System Design, 1995, v:6, n:2, pp:217-232 [Journal]
  58. Kenneth L. McMillan
    A Technique of State Space Search Based on Unfolding. [Citation Graph (0, 0)][DBLP]
    Formal Methods in System Design, 1995, v:6, n:1, pp:45-65 [Journal]
  59. Rajeev Alur, Kenneth L. McMillan, Doron Peled
    Model-Checking of Correctness Conditions for Concurrent Objects. [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 2000, v:160, n:1-2, pp:167-188 [Journal]
  60. Robert P. Kurshan, Kenneth L. McMillan
    A Structural Induction Theorem for Processes [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 1995, v:117, n:1, pp:1-11 [Journal]
  61. Kenneth L. McMillan
    A methodology for hardware verification using compositional model checking. [Citation Graph (0, 0)][DBLP]
    Sci. Comput. Program., 2000, v:37, n:1-3, pp:279-309 [Journal]
  62. Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, David L. Dill
    Symbolic model checking for sequential circuit verification. [Citation Graph (0, 0)][DBLP]
    IEEE Trans. on CAD of Integrated Circuits and Systems, 1994, v:13, n:4, pp:401-424 [Journal]
  63. Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli
    Theory of latency-insensitive design. [Citation Graph (0, 0)][DBLP]
    IEEE Trans. on CAD of Integrated Circuits and Systems, 2001, v:20, n:9, pp:1059-1076 [Journal]
  64. Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan
    Sibling-substitution-based BDD minimization using don't cares. [Citation Graph (0, 0)][DBLP]
    IEEE Trans. on CAD of Integrated Circuits and Systems, 2000, v:19, n:1, pp:44-55 [Journal]
  65. Robert P. Kurshan, Kenneth L. McMillan
    Analysis of digital circuits through symbolic reduction. [Citation Graph (0, 0)][DBLP]
    IEEE Trans. on CAD of Integrated Circuits and Systems, 1991, v:10, n:11, pp:1356-1371 [Journal]
  66. Kenneth L. McMillan
    An interpolating theorem prover. [Citation Graph (0, 0)][DBLP]
    Theor. Comput. Sci., 2005, v:345, n:1, pp:101-121 [Journal]
  67. Kenneth L. McMillan
    Toward Property-Driven Abstraction for Heap Manipulating Programs. [Citation Graph (0, 0)][DBLP]
    ATVA, 2007, pp:17-18 [Conf]
  68. Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu
    Automated Assumption Generation for Compositional Verification. [Citation Graph (0, 0)][DBLP]
    CAV, 2007, pp:420-432 [Conf]
  69. Ranjit Jhala, Kenneth L. McMillan
    Array Abstractions from Proofs. [Citation Graph (0, 0)][DBLP]
    CAV, 2007, pp:193-206 [Conf]
  70. Nina Amla, Kenneth L. McMillan
    Combining Abstraction Refinement and SAT-Based Model Checking. [Citation Graph (0, 0)][DBLP]
    TACAS, 2007, pp:405-419 [Conf]
  71. Ranjit Jhala, Kenneth L. McMillan
    Interpolant-Based Transition Relation Approximation [Citation Graph (0, 0)][DBLP]
    CoRR, 2007, v:0, n:, pp:- [Journal]

  72. Generalizing DPLL to Richer Logics. [Citation Graph (, )][DBLP]


  73. Lazy Annotation for Program Testing and Verification. [Citation Graph (, )][DBLP]


  74. Proofs, Interpolants, and Relevance Heuristics. [Citation Graph (, )][DBLP]


  75. Relevance heuristics for program analysis. [Citation Graph (, )][DBLP]


  76. Quantified Invariant Generation Using an Interpolating Saturation Prover. [Citation Graph (, )][DBLP]


  77. Interpolants and Symbolic Model Checking. [Citation Graph (, )][DBLP]


  78. What's in Common between Test, Model Checking, and Decision Procedures? [Citation Graph (, )][DBLP]


  79. Abstract Counterexamples for Non-disjunctive Abstractions. [Citation Graph (, )][DBLP]


Search in 0.004secs, Finished in 0.484secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002