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.000secs, Finished in 0.003secs