Kenneth L. McMillan

ORCID

Publication Activity (10 Years)

Years Active: 1989-2024
Publications (10 Years): 27

Top Venues

Publications

Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth L. McMillan, Risto Miikkulainen
NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks. ICLR (2024)
Kenneth L. McMillan
Toward Liveness Proofs at Scale. CAV (1) (2024)
Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck
A Case Study in Analytic Protocol Analysis in ACL2. CoRR (2023)
Max von Hippel, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck
A Formal Analysis of Karn's Algorithm. NETYS (2023)
Cole Vick, Kenneth L. McMillan
Synthesizing History and Prophecy Variables for Symbolic Model Checking. VMCAI (2023)
Yang Hu, Wenxi Wang, Sarfraz Khurshid, Kenneth L. McMillan, Mohit Tiwari
Fixing Privilege Escalations in Cloud Access Control with MaxSAT and Graph Neural Networks. ASE (2023)
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, Alex Aiken
Induction duality: primal-dual search for invariants. Proc. ACM Program. Lang. 6 (POPL) (2022)
Wenxi Wang, Yang Hu, Kenneth L. McMillan, Sarfraz Khurshid
SymMC: approximate model enumeration and counting using symmetry information for Alloy specifications. ESEC/SIGSOFT FSE (2022)
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. CoRR (2021)
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Temporal prophecy for proving temporal properties of infinite-state systems. Formal Methods Syst. Des. 57 (2) (2021)
Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth L. McMillan, Risto Miikkulainen
NeuroComb: Improving SAT Solving with Graph Neural Networks. CoRR (2021)
Kenneth L. McMillan, Oded Padon
Ivy: A Multi-modal Verification Tool for Distributed Algorithms. CAV (2) (2020)
Kenneth L. McMillan
Bayesian Interpolants as Explanations for Neural Inferences. CoRR (2020)
Lenore D. Zuck, Kenneth L. McMillan
Invisible Invariants Are Neither. From Reactive Systems to Cyber-Physical Systems (2019)
Kenneth L. McMillan, Lenore D. Zuck
Formal specification and testing of QUIC. SIGCOMM (2019)
Kenneth L. McMillan, Lenore D. Zuck
Compositional Testing of Internet Protocols. SecDev (2019)
Xinyu Wang, Greg Anderson, Isil Dillig, Kenneth L. McMillan
Learning Abstractions for Program Synthesis. CAV (1) (2018)
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. FMCAD (2018)
Kenneth L. McMillan
Eager Abstraction for Symbolic Model Checking. CAV (1) (2018)
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos
Modularity for decidability of deductive verification with applications to distributed systems. PLDI (2018)
Kenneth L. McMillan, Oded Padon
Deductive Verification in Decidable Fragments with Ivy. SAS (2018)
Xinyu Wang, Greg Anderson, Isil Dillig, Kenneth L. McMillan
Learning Abstractions for Program Synthesis. CoRR (2018)
Lenore D. Zuck, Kenneth L. McMillan, Jordan Torf
P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols. VMCAI (2018)
Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan, Mooly Sagiv
Synthesis of circular compositional program proofs via abduction. Int. J. Softw. Tools Technol. Transf. 19 (5) (2017)
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham
Ivy: safety verification by interactive generalization. PLDI (2016)
Kenneth L. McMillan
Modular specification and verification of a cache-coherent interface. FMCAD (2016)
Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. CoRR (2015)
Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko
Horn Clause Solvers for Program Verification. Fields of Logic and Computation II (2015)
Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD (2015)
Lenore D. Zuck, Kenneth L. McMillan
Reasoning about Network Topologies in Space. FPS@ETAPS (2014)
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan
Abstractions from proofs. ACM SIGPLAN Notices 49 (4S) (2014)
Kenneth L. McMillan
Lazy Annotation Revisited. CAV (2014)
Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan
Inductive invariant generation via abductive inference. OOPSLA (2013)
Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv
Synthesis of Circular Compositional Program Proofs via Abduction. TACAS (2013)
Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, Chris Hawblitzel
Differential assertion checking. ESEC/SIGSOFT FSE (2013)
Nikolaj Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. CoRR (2013)
Nikolaj Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
On Solving Universally Quantified Horn Clauses. SAS (2013)
Aws Albarghouthi, Kenneth L. McMillan
Beautiful Interpolants. CAV (2013)
Kenneth L. McMillan
Deductive Generalization. SBMF (2013)
Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken
Minimum Satisfying Assignments for SMT. CAV (2012)
Thomas Ball, Nikolaj Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes
Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. SPIN (2012)
Nikolaj Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
Program Verification as Satisfiability Modulo Theories. SMT@IJCAR (2012)
Kenneth L. McMillan
Interpolants from Z3 proofs. FMCAD (2011)
Kenneth L. McMillan
Widening and Interpolation. SAS (2011)
Kenneth L. McMillan, Lenore D. Zuck
Invisible Invariants and Abstract Interpretation. SAS (2011)
Kenneth L. McMillan
Lazy Annotation for Program Testing and Verification. CAV (2010)
Kenneth L. McMillan
What's in Common between Test, Model Checking, and Decision Procedures? FMICS (2009)
Kenneth L. McMillan, Lenore D. Zuck
Abstract Counterexamples for Non-disjunctive Abstractions. RP (2009)
Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv
Generalizing DPLL to Richer Logics. CAV (2009)
Kenneth L. McMillan
Proofs, Interpolants, and Relevance Heuristics. Haifa Verification Conference (2008)
Kenneth L. McMillan
Quantified Invariant Generation Using an Interpolating Saturation Prover. TACAS (2008)
Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu
Automated assumption generation for compositional verification. Formal Methods Syst. Des. 32 (3) (2008)
Kenneth L. McMillan
Relevance heuristics for program analysis. POPL (2008)
Ranjit Jhala, Kenneth L. McMillan
Interpolant-Based Transition Relation Approximation. Log. Methods Comput. Sci. 3 (4) (2007)
Kenneth L. McMillan
Toward Property-Driven Abstraction for Heap Manipulating Programs. ATVA (2007)
Ranjit Jhala, Kenneth L. McMillan
Array Abstractions from Proofs. CAV (2007)
Ranjit Jhala, Kenneth L. McMillan
Interpolant-Based Transition Relation Approximation CoRR (2007)
Kenneth L. McMillan
Interpolants and Symbolic Model Checking. VMCAI (2007)
Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu
Automated Assumption Generation for Compositional Verification. CAV (2007)
Nina Amla, Kenneth L. McMillan
Combining Abstraction Refinement and SAT-Based Model Checking. TACAS (2007)
Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck
Liveness by Invisible Invariants. FORTE (2006)
Ranjit Jhala, Kenneth L. McMillan
A Practical and Complete Approach to Predicate Refinement. TACAS (2006)
Kenneth L. McMillan
Lazy Abstraction with Interpolants. CAV (2006)
Kenneth L. McMillan
An interpolating theorem prover. Theor. Comput. Sci. 345 (1) (2005)
Rajeev Alur, Kenneth L. McMillan, Doron A. Peled
Deciding Global Partial-Order Properties. Formal Methods Syst. Des. 26 (1) (2005)
Ranjit Jhala, Kenneth L. McMillan
Interpolant-Based Transition Relation Approximation. CAV (2005)
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)
Kenneth L. McMillan
Applications of Craig Interpolants in Model Checking. TACAS (2005)
Kenneth L. McMillan
Applications of Craig Interpolation to Model Checking. ICATPN (2005)
Kenneth L. McMillan
Applications of Craig Interpolation to Model Checking. CSL (2004)
Nina Amla, Kenneth L. McMillan
A Hybrid of Counterexample-Based and Proof-Based Abstraction. FMCAD (2004)
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan
Abstractions from proofs. POPL (2004)
Kenneth L. McMillan
An Interpolating Theorem Prover. TACAS (2004)
Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo Medel
Experimental Analysis of Different Techniques for Bounded Model Checking. TACAS (2003)
Kenneth L. McMillan
Methods for exploiting SAT solvers in unbounded model checking. MEMOCODE (2003)
Kenneth L. McMillan, Nina Amla
Automatic Abstraction without Counterexamples. TACAS (2003)
Kenneth L. McMillan
Interpolation and SAT-Based Model Checking. CAV (2003)
Kenneth L. McMillan
Craig Interpolation and Reachability Analysis. SAS (2003)
Kenneth L. McMillan
Applying SAT Methods in Unbounded Symbolic Model Checking. CAV (2002)
Kenneth L. McMillan
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. CHARME (2001)
Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli
Theory of latency-insensitive design. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 20 (9) (2001)
Ranjit Jhala, Kenneth L. McMillan
Microarchitecture Verification by Compositional Model Checking. CAV (2001)
Kenneth L. McMillan, Shaz Qadeer, James B. Saxe
Induction in Compositional Model Checking. CAV (2000)
Rajeev Alur, Kenneth L. McMillan, Doron A. Peled
Model-Checking of Correctness Conditions for Concurrent Objects. Inf. Comput. 160 (1-2) (2000)
Kenneth L. McMillan
A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37 (1-3) (2000)
Kenneth L. McMillan
Some Strategies for Proving Theorems with a Model Checker. LICS (2000)
Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan
Sibling-substitution-based BDD minimization using don't cares. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 19 (1) (2000)
Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli
Latency Insensitive Protocols. CAV (1999)
Luca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli
A methodology for correct-by-construction latency insensitive design. ICCAD (1999)
Kenneth L. McMillan
Circular Compositional Reasoning about Liveness. CHARME (1999)
Kenneth L. McMillan
Verification of Infinite State Systems by Compositional Model Checking. CHARME (1999)
Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton
Probabilistic state space search. ICCAD (1999)
Kenneth L. McMillan
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. CAV (1998)
Kenneth L. McMillan
Proof Rules for Model Checking Systems with Data. FSTTCS (1998)
Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi
Approximation and Decomposition of Binary Decision Diagrams. DAC (1998)
Kenneth L. McMillan
Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract). FMCAD (1998)
Rajeev Alur, Kenneth L. McMillan, Doron A. Peled
Deciding Global Partial-Order Properties. ICALP (1998)
Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, Jerry Chih-Yuan Yang
Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. Formal Methods Syst. Des. 10 (2/3) (1997)
Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan
Safe BDD Minimization Using Don't Cares. DAC (1997)

Kenneth L. McMillan.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Kenneth L. McMillan