The SCEAS System
| |||||||

## Search the dblp DataBase
Kenneth L. McMillan:
[Publications]
[Author Rank by year]
[Co-authors]
[Prefers]
[Cites]
[Cited by]
## Publications of Author- 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] - Kenneth L. McMillan
**Applications of Craig Interpolation to Model Checking.**[Citation Graph (0, 0)][DBLP] ICATPN, 2005, pp:15-16 [Conf] - Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli
**Latency Insensitive Protocols.**[Citation Graph (0, 0)][DBLP] CAV, 1999, pp:123-133 [Conf] - 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] - Á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] - Ranjit Jhala, Kenneth L. McMillan
**Microarchitecture Verification by Compositional Model Checking.**[Citation Graph (0, 0)][DBLP] CAV, 2001, pp:396-410 [Conf] - Ranjit Jhala, Kenneth L. McMillan
**Interpolant-Based Transition Relation Approximation.**[Citation Graph (0, 0)][DBLP] CAV, 2005, pp:39-51 [Conf] - Kenneth L. McMillan
**Applying SAT Methods in Unbounded Symbolic Model Checking.**[Citation Graph (0, 0)][DBLP] CAV, 2002, pp:250-264 [Conf] - Kenneth L. McMillan
**Interpolation and SAT-Based Model Checking.**[Citation Graph (0, 0)][DBLP] CAV, 2003, pp:1-13 [Conf] - Kenneth L. McMillan
**Lazy Abstraction with Interpolants.**[Citation Graph (0, 0)][DBLP] CAV, 2006, pp:123-136 [Conf] - 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] - Kenneth L. McMillan
**Hierarchical Representations of Discrete Functions, with Application to Model Checking.**[Citation Graph (0, 0)][DBLP] CAV, 1994, pp:41-54 [Conf] - Kenneth L. McMillan
**Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings.**[Citation Graph (0, 0)][DBLP] CAV, 1995, pp:180-195 [Conf] - Kenneth L. McMillan
**A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking.**[Citation Graph (0, 0)][DBLP] CAV, 1996, pp:13-25 [Conf] - Kenneth L. McMillan
**A Compositional Rule for Hardware Design Refinement.**[Citation Graph (0, 0)][DBLP] CAV, 1997, pp:24-35 [Conf] - 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] - Kenneth L. McMillan, Shaz Qadeer, James B. Saxe
**Induction in Compositional Model Checking.**[Citation Graph (0, 0)][DBLP] CAV, 2000, pp:312-327 [Conf] - 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] - 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] - Kenneth L. McMillan
**Verification of Infinite State Systems by Compositional Model Checking.**[Citation Graph (0, 0)][DBLP] CHARME, 1999, pp:219-234 [Conf] - Kenneth L. McMillan
**Circular Compositional Reasoning about Liveness.**[Citation Graph (0, 0)][DBLP] CHARME, 1999, pp:342-345 [Conf] - 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] - Kenneth L. McMillan
**Applications of Craig Interpolation to Model Checking.**[Citation Graph (0, 0)][DBLP] CSL, 2004, pp:22-23 [Conf] - 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] - 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] - 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] - 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] - 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] - 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] - Kenneth L. McMillan
**Fitting Formal Methods into the Design Cycle.**[Citation Graph (0, 0)][DBLP] DAC, 1994, pp:314-319 [Conf] - 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] - 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] - 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] - 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] - Kenneth L. McMillan
**Proof Rules for Model Checking Systems with Data.**[Citation Graph (0, 0)][DBLP] FSTTCS, 1998, pp:270- [Conf] - Rajeev Alur, Kenneth L. McMillan, Doron Peled
**Deciding Global Partial-Order Properties.**[Citation Graph (0, 0)][DBLP] ICALP, 1998, pp:41-52 [Conf] - 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] - Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton
**Probabilistic state space search.**[Citation Graph (0, 0)][DBLP] ICCAD, 1999, pp:574-579 [Conf] - 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] - Janaki Akella, Kenneth L. McMillan
**Synthesizing Converters Between Finite State Protocols.**[Citation Graph (0, 0)][DBLP] ICCD, 1991, pp:410-413 [Conf] - Kenneth L. McMillan, David L. Dill
**Algorithms for Interface Timing Verification.**[Citation Graph (0, 0)][DBLP] ICCD, 1992, pp:48-51 [Conf] - 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] - 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] - Edmund M. Clarke, David E. Long, Kenneth L. McMillan
**Compositional Model Checking**[Citation Graph (0, 0)][DBLP] LICS, 1989, pp:353-362 [Conf] - Kenneth L. McMillan
**Some Strategies for Proving Theorems with a Model Checker.**[Citation Graph (0, 0)][DBLP] LICS, 2000, pp:305-306 [Conf] - Kenneth L. McMillan
**Methods for exploiting SAT solvers in unbounded model checking.**[Citation Graph (0, 0)][DBLP] MEMOCODE, 2003, pp:135-0 [Conf] - Robert P. Kurshan, Kenneth L. McMillan
**A Structural Induction Theorem for Processes.**[Citation Graph (0, 0)][DBLP] PODC, 1989, pp:239-247 [Conf] - Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan
**Abstractions from proofs.**[Citation Graph (0, 0)][DBLP] POPL, 2004, pp:232-244 [Conf] - Kenneth L. McMillan
**Craig Interpolation and Reachability Analysis.**[Citation Graph (0, 0)][DBLP] SAS, 2003, pp:336- [Conf] - 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] - Ranjit Jhala, Kenneth L. McMillan
**A Practical and Complete Approach to Predicate Refinement.**[Citation Graph (0, 0)][DBLP] TACAS, 2006, pp:459-473 [Conf] - Kenneth L. McMillan
**An Interpolating Theorem Prover.**[Citation Graph (0, 0)][DBLP] TACAS, 2004, pp:16-30 [Conf] - Kenneth L. McMillan
**Applications of Craig Interpolants in Model Checking.**[Citation Graph (0, 0)][DBLP] TACAS, 2005, pp:1-12 [Conf] - Kenneth L. McMillan, Nina Amla
**Automatic Abstraction without Counterexamples.**[Citation Graph (0, 0)][DBLP] TACAS, 2003, pp:2-17 [Conf] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - Kenneth L. McMillan
**An interpolating theorem prover.**[Citation Graph (0, 0)][DBLP] Theor. Comput. Sci., 2005, v:345, n:1, pp:101-121 [Journal] - Kenneth L. McMillan
**Toward Property-Driven Abstraction for Heap Manipulating Programs.**[Citation Graph (0, 0)][DBLP] ATVA, 2007, pp:17-18 [Conf] - Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu
**Automated Assumption Generation for Compositional Verification.**[Citation Graph (0, 0)][DBLP] CAV, 2007, pp:420-432 [Conf] - Ranjit Jhala, Kenneth L. McMillan
**Array Abstractions from Proofs.**[Citation Graph (0, 0)][DBLP] CAV, 2007, pp:193-206 [Conf] - Nina Amla, Kenneth L. McMillan
**Combining Abstraction Refinement and SAT-Based Model Checking.**[Citation Graph (0, 0)][DBLP] TACAS, 2007, pp:405-419 [Conf] - Ranjit Jhala, Kenneth L. McMillan
**Interpolant-Based Transition Relation Approximation**[Citation Graph (0, 0)][DBLP] CoRR, 2007, v:0, n:, pp:- [Journal] **Generalizing DPLL to Richer Logics.**[Citation Graph (, )][DBLP]**Lazy Annotation for Program Testing and Verification.**[Citation Graph (, )][DBLP]**Proofs, Interpolants, and Relevance Heuristics.**[Citation Graph (, )][DBLP]**Relevance heuristics for program analysis.**[Citation Graph (, )][DBLP]**Quantified Invariant Generation Using an Interpolating Saturation Prover.**[Citation Graph (, )][DBLP]**Interpolants and Symbolic Model Checking.**[Citation Graph (, )][DBLP]**What's in Common between Test, Model Checking, and Decision Procedures?**[Citation Graph (, )][DBLP]**Abstract Counterexamples for Non-disjunctive Abstractions.**[Citation Graph (, )][DBLP]
Search in 0.023secs, Finished in 0.028secs | |||||||

| |||||||

| |||||||

System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002 for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002 |