| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Kenneth L. McMillan, Lenore D. Zuck |
Invisible Invariants and Abstract Interpretation.  |
SAS  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Widening and Interpolation. |
SAS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Lazy Annotation for Program Testing and Verification. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
What's in Common between Test, Model Checking, and Decision Procedures? |
FMICS |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan, Lenore D. Zuck |
Abstract Counterexamples for Non-disjunctive Abstractions. |
RP |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv |
Generalizing DPLL to Richer Logics. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu |
Automated assumption generation for compositional verification. |
Formal Methods in System Design |
2008 |
DBLP DOI BibTeX RDF |
L*, Model checking, Formal verification, Decision tree, SAT, Compositional verification, Assume-guarantee |
| 1 | Kenneth L. McMillan |
Quantified Invariant Generation Using an Interpolating Saturation Prover. |
TACAS |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Relevance heuristics for program analysis. |
POPL |
2008 |
DBLP DOI BibTeX RDF |
model checking, abstract interpretation, craig interpolation |
| 1 | Kenneth L. McMillan |
Proofs, Interpolants, and Relevance Heuristics. |
Haifa Verification Conference |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranjit Jhala, Kenneth L. McMillan |
Interpolant-Based Transition Relation Approximation. |
Logical Methods in Computer Science |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranjit Jhala, Kenneth L. McMillan |
Interpolant-Based Transition Relation Approximation |
CoRR |
2007 |
DBLP BibTeX RDF |
|
| 1 | Nina Amla, Kenneth L. McMillan |
Combining Abstraction Refinement and SAT-Based Model Checking. |
TACAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Toward Property-Driven Abstraction for Heap Manipulating Programs. |
ATVA |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranjit Jhala, Kenneth L. McMillan |
Array Abstractions from Proofs. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu |
Automated Assumption Generation for Compositional Verification. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Interpolants and Symbolic Model Checking. |
VMCAI |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck |
Liveness by Invisible Invariants. |
FORTE |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranjit Jhala, Kenneth L. McMillan |
A Practical and Complete Approach to Predicate Refinement. |
TACAS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Lazy Abstraction with Interpolants. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
An interpolating theorem prover. |
Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Kenneth L. McMillan, Doron Peled |
Deciding Global Partial-Order Properties. |
Formal Methods in System Design |
2005 |
DBLP DOI BibTeX RDF |
partial order logics, model checking, concurrency, temporal logics |
| 1 | Kenneth L. McMillan |
Applications of Craig Interpolation to Model Checking. |
ICATPN |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Applications of Craig Interpolants in Model Checking. |
TACAS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranjit Jhala, Kenneth L. McMillan |
Interpolant-Based Transition Relation Approximation. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
An Interpolating Theorem Prover. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Nina Amla, Kenneth L. McMillan |
A Hybrid of Counterexample-Based and Proof-Based Abstraction. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan |
Abstractions from proofs. |
POPL |
2004 |
DBLP DOI BibTeX RDF |
counterexample analysis, software model checking, predicate abstraction |
| 1 | Kenneth L. McMillan |
Applications of Craig Interpolation to Model Checking. |
CSL |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Methods for exploiting SAT solvers in unbounded model checking. |
MEMOCODE |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan, Nina Amla |
Automatic Abstraction without Counterexamples. |
TACAS |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo Medel |
Experimental Analysis of Different Techniques for Bounded Model Checking. |
TACAS |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Interpolation and SAT-Based Model Checking. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Craig Interpolation and Reachability Analysis. |
SAS |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Applying SAT Methods in Unbounded Symbolic Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli |
Theory of latency-insensitive design. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranjit Jhala, Kenneth L. McMillan |
Microarchitecture Verification by Compositional Model Checking. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
A methodology for hardware verification using compositional model checking. |
Sci. Comput. Program. |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Kenneth L. McMillan, Doron Peled |
Model-Checking of Correctness Conditions for Concurrent Objects. |
Inf. Comput. |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan, Shaz Qadeer, James B. Saxe |
Induction in Compositional Model Checking. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Some Strategies for Proving Theorems with a Model Checker. |
LICS |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Verification of Infinite State Systems by Compositional Model Checking. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Circular Compositional Reasoning about Liveness. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli |
Latency Insensitive Protocols. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton |
Probabilistic state space search. |
ICCAD |
1999 |
DBLP BibTeX RDF |
|
| 1 | Luca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli |
A methodology for correct-by-construction latency insensitive design. |
ICCAD |
1999 |
DBLP BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract). |
FMCAD |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Kenneth L. McMillan, Doron Peled |
Deciding Global Partial-Order Properties. |
ICALP |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi |
Approximation and Decomposition of Binary Decision Diagrams. |
DAC |
1998 |
DBLP DOI BibTeX RDF |
transceiver, spread spectrum communication, RF CMOS, digital radio, ISM frequency band |
| 1 | Kenneth L. McMillan |
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Proof Rules for Model Checking Systems with Data. |
FSTTCS |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan |
Safe BDD Minimization Using Don't Cares. |
DAC |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
A Compositional Rule for Hardware Design Refinement. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vassili Hartonas-Garmhausen |
Symbolic Model Checking. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Kenneth L. McMillan, Doron Peled |
Model-Checking of Correctness Conditions for Concurrent Objects. |
LICS |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert P. Kurshan, Kenneth L. McMillan |
A Structural Induction Theorem for Processes |
Inf. Comput. |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
A Technique of State Space Search Based on Unfolding. |
Formal Methods in System Design |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao |
Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. |
DAC |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Ásgeir Th. Eiríksson, Kenneth L. McMillan |
Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study. |
CAV |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. |
CAV |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick C. McGeer, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli, Patrick Scaglia |
Fast discrete function evaluation using decision diagrams. |
ICCAD |
1995 |
DBLP DOI BibTeX RDF |
address lookups, cycle-based logic simulation, decision-diagram based function evaluation, fast discrete function evaluation, latch ports, orders-of-magnitude potential speedup, output ports, logic design, memory hierarchy, logic CAD, decision theory, circuit analysis computing, memory bandwidth, table lookup, digital circuits, logic simulators, logic function, function evaluation, multi-valued decision diagrams |
| 1 | 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 |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Fitting Formal Methods into the Design Cycle. |
DAC |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Hierarchical Representations of Discrete Functions, with Application to Model Checking. |
CAV |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Symbolic model checking. |
|
1993 |
RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP BibTeX RDF |
|
| 1 | 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. |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan |
Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. |
CAV |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan, David L. Dill |
Algorithms for Interface Timing Verification. |
ICCD |
1992 |
DBLP BibTeX RDF |
|
| 1 | Robert P. Kurshan, Kenneth L. McMillan |
Analysis of digital circuits through symbolic reduction. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
1991 |
DBLP DOI BibTeX RDF |
|
| 1 | Janaki Akella, Kenneth L. McMillan |
Synthesizing Converters Between Finite State Protocols. |
ICCD |
1991 |
DBLP BibTeX RDF |
|
| 1 | Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill |
Sequential Circuit Verification Using Symbolic Model Checking. |
DAC |
1990 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert P. Kurshan, Kenneth L. McMillan |
A Structural Induction Theorem for Processes. |
PODC |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, David E. Long, Kenneth L. McMillan |
Compositional Model Checking |
LICS |
1989 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")