Kenneth L. McMillan

138 papers A* 43A 12B 18C 5Journal 33Unranked 24

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols. Commun. ACM David A. Basin, Nate Foster, Kenneth L. McMillan, Kedar S. Namjoshi, Cristina Nita-Rotaru, Jonathan M. Smith, Pamela Zave, Lenore D. Zuck
2025	J	`jnl`	It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols. CoRR David A. Basin, Nate Foster, Kenneth L. McMillan, Kedar S. Namjoshi, Cristina Nita-Rotaru, Jonathan M. Smith, Pamela Zave, Lenore D. Zuck
2024	J	`jnl`	Invariant Checking for SMT-Based Systems with Quantifiers. ACM Trans. Comput. Log. Gianluca Redondi, Alessandro Cimatti, Alberto Griggio, Kenneth L. McMillan
2024	J	`jnl`	Invariant Checking for SMT-based Systems with Quantifiers. CoRR Gianluca Redondi, Alessandro Cimatti, Alberto Griggio, Kenneth L. McMillan
2024	A*	`conf`	NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks. ICLR Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth L. McMillan, Risto Miikkulainen
2024	—	`conf`	Toward Liveness Proofs at Scale. CAV (1) Kenneth L. McMillan
2023	—	`conf`	A Case Study in Analytic Protocol Analysis in ACL2. ACL2 Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck
2023	—	`conf`	A Formal Analysis of Karn's Algorithm. NETYS Max von Hippel, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck
2023	J	`jnl`	Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols. Proc. ACM Program. Lang. Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv
2023	A*	`conf`	Fixing Privilege Escalations in Cloud Access Control with MaxSAT and Graph Neural Networks. ASE Yang Hu, Wenxi Wang, Sarfraz Khurshid, Kenneth L. McMillan, Mohit Tiwari
2023	B	`conf`	Synthesizing History and Prophecy Variables for Symbolic Model Checking. VMCAI Cole Vick, Kenneth L. McMillan
2023	J	`jnl`	Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112). Dagstuhl Reports Swen Jacobs, Kenneth L. McMillan, Roopsha Samanta, Ilya Sergey
2022	J	`jnl`	Induction duality: primal-dual search for invariants. Proc. ACM Program. Lang. Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, Alex Aiken
2022	—	`conf`	SymMC: approximate model enumeration and counting using symmetry information for Alloy specifications. ESEC/SIGSOFT FSE Wenxi Wang, Yang Hu, Kenneth L. McMillan, Sarfraz Khurshid
2021	J	`jnl`	NeuroComb: Improving SAT Solving with Graph Neural Networks. CoRR Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth L. McMillan, Risto Miikkulainen
2021	J	`jnl`	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. CoRR Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2021	J	`jnl`	Temporal prophecy for proving temporal properties of infinite-state systems. Formal Methods Syst. Des. Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2020	J	`jnl`	Bayesian Interpolants as Explanations for Neural Inferences. CoRR Kenneth L. McMillan
2020	—	`conf`	Ivy: A Multi-modal Verification Tool for Distributed Algorithms. CAV (2) Kenneth L. McMillan, Oded Padon
2019	—	`conf`	Compositional Testing of Internet Protocols. SecDev Kenneth L. McMillan, Lenore D. Zuck
2019	A*	`conf`	Formal specification and testing of QUIC. SIGCOMM Kenneth L. McMillan, Lenore D. Zuck
2019	—	`conf`	Invisible Invariants Are Neither. From Reactive Systems to Cyber-Physical Systems Lenore D. Zuck, Kenneth L. McMillan
2018	B	`conf`	Deductive Verification in Decidable Fragments with Ivy. SAS Kenneth L. McMillan, Oded Padon
2018	—	`conf`	Eager Abstraction for Symbolic Model Checking. CAV (1) Kenneth L. McMillan
2018	—	`ch.`	Interpolation and Model Checking. Handbook of Model Checking Kenneth L. McMillan
2018	—	`conf`	Learning Abstractions for Program Synthesis. CAV (1) Xinyu Wang, Greg Anderson, Isil Dillig, Kenneth L. McMillan
2018	J	`jnl`	Learning Abstractions for Program Synthesis. CoRR Xinyu Wang, Greg Anderson, Isil Dillig, Kenneth L. McMillan
2018	A*	`conf`	Modularity for decidability of deductive verification with applications to distributed systems. PLDI Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos
2018	B	`conf`	P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols. VMCAI Lenore D. Zuck, Kenneth L. McMillan, Jordan Torf
2018	B	`conf`	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. FMCAD Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2017	J	`jnl`	Synthesis of circular compositional program proofs via abduction. Int. J. Softw. Tools Technol. Transf. Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan, Mooly Sagiv
2016	A*	`conf`	Ivy: safety verification by interactive generalization. PLDI Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham
2016	B	`conf`	Modular specification and verification of a cache-coherent interface. FMCAD Kenneth L. McMillan
2015	B	`conf`	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan
2015	J	`jnl`	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. CoRR Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan
2015	—	`conf`	Horn Clause Solvers for Program Verification. Fields of Logic and Computation II Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko
2014	J	`jnl`	Abstractions from proofs. ACM SIGPLAN Notices Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan
2014	—	`ed.`	LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings LPAR (short papers) Kenneth L. McMillan, Aart Middeldorp, Geoff Sutcliffe, Andrei Voronkov
2014	A*	`conf`	Lazy Annotation Revisited. CAV Kenneth L. McMillan
2014	—	`conf`	Reasoning about Network Topologies in Space. FPS@ETAPS Lenore D. Zuck, Kenneth L. McMillan
2014	B	`ed.`	Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings VMCAI Kenneth L. McMillan, Xavier Rival
2013	A*	`conf`	Beautiful Interpolants. CAV Aws Albarghouthi, Kenneth L. McMillan
2013	—	`conf`	Deductive Generalization. SBMF Kenneth L. McMillan
2013	—	`conf`	Differential assertion checking. ESEC/SIGSOFT FSE Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, Chris Hawblitzel
2013	J	`jnl`	Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. CoRR Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
2013	A	`conf`	Inductive invariant generation via abductive inference. OOPSLA Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan
2013	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings LPAR Kenneth L. McMillan, Aart Middeldorp, Andrei Voronkov
2013	B	`conf`	On Solving Universally Quantified Horn Clauses. SAS Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
2013	A	`conf`	Synthesis of Circular Compositional Program Proofs via Abduction. TACAS Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv
2012	—	`conf`	Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. SPIN Thomas Ball, Nikolaj S. Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes
2012	A*	`conf`	Minimum Satisfying Assignments for SMT. CAV Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken
2012	—	`conf`	Program Verification as Satisfiability Modulo Theories. SMT@IJCAR Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
2011	B	`conf`	Interpolants from Z3 proofs. FMCAD Kenneth L. McMillan
2011	B	`conf`	Invisible Invariants and Abstract Interpretation. SAS Kenneth L. McMillan, Lenore D. Zuck
2011	B	`conf`	Widening and Interpolation. SAS Kenneth L. McMillan
2010	A*	`conf`	Lazy Annotation for Program Testing and Verification. CAV Kenneth L. McMillan
2009	—	`conf`	Abstract Counterexamples for Non-disjunctive Abstractions. RP Kenneth L. McMillan, Lenore D. Zuck
2009	A*	`conf`	Generalizing DPLL to Richer Logics. CAV Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv
2009	C	`conf`	What's in Common between Test, Model Checking, and Decision Procedures? FMICS Kenneth L. McMillan
2008	J	`jnl`	Automated assumption generation for compositional verification. Formal Methods Syst. Des. Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu
2008	—	`conf`	Proofs, Interpolants, and Relevance Heuristics. Haifa Verification Conference Kenneth L. McMillan
2008	A	`conf`	Quantified Invariant Generation Using an Interpolating Saturation Prover. TACAS Kenneth L. McMillan
2008	A*	`conf`	Relevance heuristics for program analysis. POPL Kenneth L. McMillan
2007	A*	`conf`	Array Abstractions from Proofs. CAV Ranjit Jhala, Kenneth L. McMillan
2007	A*	`conf`	Automated Assumption Generation for Compositional Verification. CAV Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu
2007	A	`conf`	Combining Abstraction Refinement and SAT-Based Model Checking. TACAS Nina Amla, Kenneth L. McMillan
2007	J	`jnl`	Interpolant-Based Transition Relation Approximation CoRR Ranjit Jhala, Kenneth L. McMillan
2007	J	`jnl`	Interpolant-Based Transition Relation Approximation. Log. Methods Comput. Sci. Ranjit Jhala, Kenneth L. McMillan
2007	B	`conf`	Interpolants and Symbolic Model Checking. VMCAI Kenneth L. McMillan
2007	B	`conf`	Toward Property-Driven Abstraction for Heap Manipulating Programs. ATVA Kenneth L. McMillan
2006	A	`conf`	A Practical and Complete Approach to Predicate Refinement. TACAS Ranjit Jhala, Kenneth L. McMillan
2006	A*	`conf`	Lazy Abstraction with Interpolants. CAV Kenneth L. McMillan
2006	C	`conf`	Liveness by Invisible Invariants. FORTE Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck
2005	—	`conf`	An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment. CHARME Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, Kenneth L. McMillan
2005	J	`jnl`	An interpolating theorem prover. Theor. Comput. Sci. Kenneth L. McMillan
2005	A	`conf`	Applications of Craig Interpolants in Model Checking. TACAS Kenneth L. McMillan
2005	—	`conf`	Applications of Craig Interpolation to Model Checking. ICATPN Kenneth L. McMillan
2005	J	`jnl`	Deciding Global Partial-Order Properties. Formal Methods Syst. Des. Rajeev Alur, Kenneth L. McMillan, Doron A. Peled
2005	A*	`conf`	Interpolant-Based Transition Relation Approximation. CAV Ranjit Jhala, Kenneth L. McMillan
2004	B	`conf`	A Hybrid of Counterexample-Based and Proof-Based Abstraction. FMCAD Nina Amla, Kenneth L. McMillan
2004	A*	`conf`	Abstractions from proofs. POPL Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan
2004	A	`conf`	An Interpolating Theorem Prover. TACAS Kenneth L. McMillan
2004	B	`conf`	Applications of Craig Interpolation to Model Checking. CSL Kenneth L. McMillan
2003	A	`conf`	Automatic Abstraction without Counterexamples. TACAS Kenneth L. McMillan, Nina Amla
2003	B	`conf`	Craig Interpolation and Reachability Analysis. SAS Kenneth L. McMillan
2003	A	`conf`	Experimental Analysis of Different Techniques for Bounded Model Checking. TACAS Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo H. Medel
2003	A*	`conf`	Interpolation and SAT-Based Model Checking. CAV Kenneth L. McMillan
2003	C	`conf`	Methods for exploiting SAT solvers in unbounded model checking. MEMOCODE Kenneth L. McMillan
2002	A*	`conf`	Applying SAT Methods in Unbounded Symbolic Model Checking. CAV Kenneth L. McMillan
2001	A*	`conf`	Microarchitecture Verification by Compositional Model Checking. CAV Ranjit Jhala, Kenneth L. McMillan
2001	—	`conf`	Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. CHARME Kenneth L. McMillan
2001	J	`jnl`	Theory of latency-insensitive design. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli
2000	J	`jnl`	A methodology for hardware verification using compositional model checking. Sci. Comput. Program. Kenneth L. McMillan
2000	A*	`conf`	Induction in Compositional Model Checking. CAV Kenneth L. McMillan, Shaz Qadeer, James B. Saxe
2000	J	`jnl`	Model-Checking of Correctness Conditions for Concurrent Objects. Inf. Comput. Rajeev Alur, Kenneth L. McMillan, Doron A. Peled
2000	J	`jnl`	Sibling-substitution-based BDD minimization using don't cares. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan
2000	A*	`conf`	Some Strategies for Proving Theorems with a Model Checker. LICS Kenneth L. McMillan
1999	A	`conf`	A methodology for correct-by-construction latency insensitive design. ICCAD Luca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli
1999	—	`conf`	Circular Compositional Reasoning about Liveness. CHARME Kenneth L. McMillan
1999	A*	`conf`	Latency Insensitive Protocols. CAV Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli
1999	A	`conf`	Probabilistic state space search. ICCAD Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton
1999	—	`conf`	Verification of Infinite State Systems by Compositional Model Checking. CHARME Kenneth L. McMillan
1998	A*	`conf`	Approximation and Decomposition of Binary Decision Diagrams. DAC Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi
1998	A*	`conf`	Deciding Global Partial-Order Properties. ICALP Rajeev Alur, Kenneth L. McMillan, Doron A. Peled
1998	B	`conf`	Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract). FMCAD Kenneth L. McMillan
1998	—	`conf`	Proof Rules for Model Checking Systems with Data. FSTTCS Kenneth L. McMillan
1998	A*	`conf`	Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. CAV Kenneth L. McMillan
1997	A*	`conf`	A Compositional Rule for Hardware Design Refinement. CAV Kenneth L. McMillan
1997	A*	`conf`	Safe BDD Minimization Using Don't Cares. DAC Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan
1997	J	`jnl`	Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. Formal Methods Syst. Des. Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, Jerry Chih-Yuan Yang
1996	A*	`conf`	A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. CAV Kenneth L. McMillan
1996	A*	`conf`	Engineering Change in a Non-Deterministic FSM Setting. DAC Sunil P. Khatri, Amit Narayan, Sriram C. Krishnan, Kenneth L. McMillan, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli
1996	A*	`conf`	Model-Checking of Correctness Conditions for Concurrent Objects. LICS Rajeev Alur, Kenneth L. McMillan, Doron A. Peled
1996	A*	`conf`	Symbolic Model Checking. CAV Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vasiliki Hartonas-Garmhausen
1995	J	`jnl`	A Structural Induction Theorem for Processes Inf. Comput. Robert P. Kurshan, Kenneth L. McMillan
1995	J	`jnl`	A Technique of State Space Search Based on Unfolding. Formal Methods Syst. Des. Kenneth L. McMillan
1995	A*	`conf`	Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao
1995	A	`conf`	Fast discrete function evaluation using decision diagrams. ICCAD Patrick C. McGeer, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli, Patrick Scaglia
1995	A*	`conf`	Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. CAV Kenneth L. McMillan
1995	A*	`conf`	Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study. CAV Ásgeir Th. Eiríksson, Kenneth L. McMillan
1995	J	`jnl`	Verification of the Futurebus+ Cache Coherence Protocol. Formal Methods Syst. Des. Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness
1994	A*	`conf`	Fitting Formal Methods into the Design Cycle. DAC Kenneth L. McMillan
1994	A*	`conf`	Hierarchical Representations of Discrete Functions, with Application to Model Checking. CAV Kenneth L. McMillan
1994	A*	`conf`	Panel: Complex System Verification: The Challenge Ahead. DAC Ronald Collett, Mike Gianfagna, Michel Courtoy, Martin Baynes, Johan Van Ginderdeuren, Kenneth L. McMillan, Stephen Ricca, Alberto L. Sangiovanni-Vincentelli, Steve Sapiro, Naeem Zafar
1994	J	`jnl`	Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, David L. Dill
1993	A*	`conf`	Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. DAC Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, Jerry Chih-Yuan Yang
1993	—	`book`	Symbolic model checking. Kenneth L. McMillan
1993	—	`conf`	Verification of the Futurebus+ Cache Coherence Protocol. CHDL Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness
1992	C	`conf`	Algorithms for Interface Timing Verification. ICCD Kenneth L. McMillan, David L. Dill
1992	J	`jnl`	Symbolic Model Checking: 10^20 States and Beyond Inf. Comput. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang
1992	A*	`conf`	Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. CAV Kenneth L. McMillan
1991	J	`jnl`	A language for compositional specification and verification of finite state hardware controllers. Proc. IEEE Edmund M. Clarke, David E. Long, Kenneth L. McMillan
1991	J	`jnl`	Analysis of digital circuits through symbolic reduction. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Robert P. Kurshan, Kenneth L. McMillan
1991	C	`conf`	Synthesizing Converters Between Finite State Protocols. ICCD Janaki Akella, Kenneth L. McMillan
1990	A*	`conf`	Sequential Circuit Verification Using Symbolic Model Checking. DAC Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill
1990	A*	`conf`	Symbolic Model Checking: 10^20 States and Beyond LICS Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang
1989	A*	`conf`	A Structural Induction Theorem for Processes. PODC Robert P. Kurshan, Kenneth L. McMillan
1989	A*	`conf`	Compositional Model Checking LICS Edmund M. Clarke, David E. Long, Kenneth L. McMillan