Kenneth L. McMillan

According to our database1, Kenneth L. McMillan authored at least 102 papers between 1989 and 2020.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2020
Bayesian Interpolants as Explanations for Neural Inferences.
CoRR, 2020

Ivy: A Multi-modal Verification Tool for Distributed Algorithms.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019
Formal specification and testing of QUIC.
Proceedings of the ACM Special Interest Group on Data Communication, 2019

Compositional Testing of Internet Protocols.
Proceedings of the 2019 IEEE Cybersecurity Development, 2019

Invisible Invariants Are Neither.
Proceedings of the From Reactive Systems to Cyber-Physical Systems, 2019

2018
Interpolation and Model Checking.
Proceedings of the Handbook of Model Checking., 2018

P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Deductive Verification in Decidable Fragments with Ivy.
Proceedings of the Static Analysis - 25th International Symposium, 2018

Modularity for decidability of deductive verification with applications to distributed systems.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems.
Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Learning Abstractions for Program Synthesis.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Eager Abstraction for Symbolic Model Checking.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017
Synthesis of circular compositional program proofs via abduction.
Int. J. Softw. Tools Technol. Transf., 2017

2016
Ivy: safety verification by interactive generalization.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Modular specification and verification of a cache-coherent interface.
Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

2015
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Horn Clause Solvers for Program Verification.
Proceedings of the Fields of Logic and Computation II, 2015

2014
Reasoning about Network Topologies in Space.
Proceedings of the From Programs to Systems. The Systems perspective in Computing, 2014

Lazy Annotation Revisited.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types.
CoRR, 2013

Differential assertion checking.
Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013

Deductive Generalization.
Proceedings of the Formal Methods: Foundations and Applications - 16th Brazilian Symposium, 2013

On Solving Universally Quantified Horn Clauses.
Proceedings of the Static Analysis - 20th International Symposium, 2013

Inductive invariant generation via abductive inference.
Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

Beautiful Interpolants.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012
Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials.
Proceedings of the Model Checking Software - 19th International Workshop, 2012

Minimum Satisfying Assignments for SMT.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Program Verification as Satisfiability Modulo Theories.
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011
Invisible Invariants and Abstract Interpretation.
Proceedings of the Static Analysis - 18th International Symposium, 2011

Widening and Interpolation.
Proceedings of the Static Analysis - 18th International Symposium, 2011

Interpolants from Z3 proofs.
Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

2010
Lazy Annotation for Program Testing and Verification.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Abstract Counterexamples for Non-disjunctive Abstractions.
Proceedings of the Reachability Problems, 3rd International Workshop, 2009

What's in Common between Test, Model Checking, and Decision Procedures?
Proceedings of the Formal Methods for Industrial Critical Systems, 2009

Generalizing DPLL to Richer Logics.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
Automated assumption generation for compositional verification.
Formal Methods Syst. Des., 2008

Quantified Invariant Generation Using an Interpolating Saturation Prover.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Relevance heuristics for program analysis.
Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

Proofs, Interpolants, and Relevance Heuristics.
Proceedings of the Hardware and Software: Verification and Testing, 2008

2007
Interpolant-Based Transition Relation Approximation.
Log. Methods Comput. Sci., 2007

Interpolants and Symbolic Model Checking.
Proceedings of the Verification, 2007

Combining Abstraction Refinement and SAT-Based Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Array Abstractions from Proofs.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Toward Property-Driven Abstraction for Heap Manipulating Programs.
Proceedings of the Automated Technology for Verification and Analysis, 2007

2006
A Practical and Complete Approach to Predicate Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Liveness by Invisible Invariants.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2006

Lazy Abstraction with Interpolants.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005
An interpolating theorem prover.
Theor. Comput. Sci., 2005

Deciding Global Partial-Order Properties.
Formal Methods Syst. Des., 2005

Applications of Craig Interpolants in Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment.
Proceedings of the Correct Hardware Design and Verification Methods, 2005

Applications of Craig Interpolation to Model Checking.
Proceedings of the Applications and Theory of Petri Nets 2005, 2005

2004
Abstractions from proofs.
Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

A Hybrid of Counterexample-Based and Proof-Based Abstraction.
Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

2003
Automatic Abstraction without Counterexamples.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Experimental Analysis of Different Techniques for Bounded Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Craig Interpolation and Reachability Analysis.
Proceedings of the Static Analysis, 10th International Symposium, 2003

Methods for exploiting SAT solvers in unbounded model checking.
Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003

Interpolation and SAT-Based Model Checking.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002
Applying SAT Methods in Unbounded Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
Theory of latency-insensitive design.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2001

Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 2001

Microarchitecture Verification by Compositional Model Checking.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000
Sibling-substitution-based BDD minimization using don't cares.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2000

A methodology for hardware verification using compositional model checking.
Sci. Comput. Program., 2000

Model-Checking of Correctness Conditions for Concurrent Objects.
Inf. Comput., 2000

Some Strategies for Proving Theorems with a Model Checker.
Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

Induction in Compositional Model Checking.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999
Probabilistic state space search.
Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

A methodology for correct-by-construction latency insensitive design.
Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

Circular Compositional Reasoning about Liveness.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

Verification of Infinite State Systems by Compositional Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

Latency Insensitive Protocols.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998
Proof Rules for Model Checking Systems with Data.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1998

Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract).
Proceedings of the Formal Methods in Computer-Aided Design, 1998

Approximation and Decomposition of Binary Decision Diagrams.
Proceedings of the 35th Conference on Design Automation, 1998

Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997
Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping.
Formal Methods Syst. Des., 1997

Safe BDD Minimization Using Don't Cares.
Proceedings of the 34st Conference on Design Automation, 1997

A Compositional Rule for Hardware Design Refinement.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997

1996
Engineering Change in a Non-Deterministic FSM Setting.
Proceedings of the 33st Conference on Design Automation, 1996

A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995
A Structural Induction Theorem for Processes
Inf. Comput., February, 1995

A Technique of State Space Search Based on Unfolding.
Formal Methods Syst. Des., 1995

Verification of the Futurebus+ Cache Coherence Protocol.
Formal Methods Syst. Des., 1995

Fast discrete function evaluation using decision diagrams.
Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, 1995

Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking.
Proceedings of the 32st Conference on Design Automation, 1995

Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings.
Proceedings of the Computer Aided Verification, 1995

Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study.
Proceedings of the Computer Aided Verification, 1995

1994
Symbolic model checking for sequential circuit verification.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1994

Fitting Formal Methods into the Design Cycle.
Proceedings of the 31st Conference on Design Automation, 1994

Panel: Complex System Verification: The Challenge Ahead.
Proceedings of the 31st Conference on Design Automation, 1994

Hierarchical Representations of Discrete Functions, with Application to Model Checking.
Proceedings of the Computer Aided Verification, 6th International Conference, 1994

1993
Symbolic model checking.
Kluwer, ISBN: 978-1-4615-3190-6, 1993

1992
Symbolic Model Checking: 10^20 States and Beyond
Inf. Comput., June, 1992

Algorithms for Interface Timing Verification.
Proceedings of the Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1992

Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits.
Proceedings of the Computer Aided Verification, Fourth International Workshop, 1992

1991
Analysis of digital circuits through symbolic reduction.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1991

Synthesizing Converters Between Finite State Protocols.
Proceedings of the Proceedings 1991 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1991

1990
Sequential Circuit Verification Using Symbolic Model Checking.
Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, 1990

1989
Compositional Model Checking
Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989


  Loading...