default search action
Kenneth L. McMillan
Person information
- affiliation: University of Texas Austin, Austin, USA
- affiliation: Microsoft Research, Redmond, USA
- award (1998): Paris Kanellakis Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [c100]Kenneth L. McMillan:
Toward Liveness Proofs at Scale. CAV (1) 2024: 255-276 - [c99]Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth L. McMillan, Risto Miikkulainen:
NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks. ICLR 2024 - 2023
- [j21]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): 1878-1904 (2023) - [c98]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: 104-115 - [c97]Max von Hippel, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck:
A Formal Analysis of Karn's Algorithm. NETYS 2023: 43-61 - [c96]Cole Vick, Kenneth L. McMillan:
Synthesizing History and Prophecy Variables for Symbolic Model Checking. VMCAI 2023: 320-340 - [c95]Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck:
A Case Study in Analytic Protocol Analysis in ACL2. ACL2 2023: 50-66 - 2022
- [j20]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): 1-29 (2022) - [c94]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: 1209-1220 - 2021
- [j19]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): 246-269 (2021) - [i7]Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham:
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. CoRR abs/2106.00966 (2021) - [i6]Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth L. McMillan, Risto Miikkulainen:
NeuroComb: Improving SAT Solving with Graph Neural Networks. CoRR abs/2110.14053 (2021) - 2020
- [c93]Kenneth L. McMillan, Oded Padon:
Ivy: A Multi-modal Verification Tool for Distributed Algorithms. CAV (2) 2020: 190-202 - [i5]Kenneth L. McMillan:
Bayesian Interpolants as Explanations for Neural Inferences. CoRR abs/2004.04198 (2020)
2010 – 2019
- 2019
- [c92]Lenore D. Zuck, Kenneth L. McMillan:
Invisible Invariants Are Neither. From Reactive Systems to Cyber-Physical Systems 2019: 57-72 - [c91]Kenneth L. McMillan, Lenore D. Zuck:
Compositional Testing of Internet Protocols. SecDev 2019: 161-174 - [c90]Kenneth L. McMillan, Lenore D. Zuck:
Formal specification and testing of QUIC. SIGCOMM 2019: 227-240 - 2018
- [c89]Kenneth L. McMillan:
Eager Abstraction for Symbolic Model Checking. CAV (1) 2018: 191-208 - [c88]Xinyu Wang, Greg Anderson, Isil Dillig, Kenneth L. McMillan:
Learning Abstractions for Program Synthesis. CAV (1) 2018: 407-426 - [c87]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: 1-11 - [c86]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: 662-677 - [c85]Kenneth L. McMillan, Oded Padon:
Deductive Verification in Decidable Fragments with Ivy. SAS 2018: 43-55 - [c84]Lenore D. Zuck, Kenneth L. McMillan, Jordan Torf:
P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols. VMCAI 2018: 336-357 - [p1]Kenneth L. McMillan:
Interpolation and Model Checking. Handbook of Model Checking 2018: 421-446 - [i4]Xinyu Wang, Greg Anderson, Isil Dillig, Kenneth L. McMillan:
Learning Abstractions for Program Synthesis. CoRR abs/1804.04152 (2018) - 2017
- [j18]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): 535-547 (2017) - 2016
- [c83]Kenneth L. McMillan:
Modular specification and verification of a cache-coherent interface. FMCAD 2016: 109-116 - [c82]Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham:
Ivy: safety verification by interactive generalization. PLDI 2016: 614-630 - 2015
- [c81]Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko:
Horn Clause Solvers for Program Verification. Fields of Logic and Computation II 2015: 24-51 - [c80]Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96 - [i3]Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. CoRR abs/1508.01288 (2015) - 2014
- [j17]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan:
Abstractions from proofs. ACM SIGPLAN Notices 49(4S): 79-91 (2014) - [c79]Kenneth L. McMillan:
Lazy Annotation Revisited. CAV 2014: 243-259 - [c78]Lenore D. Zuck, Kenneth L. McMillan:
Reasoning about Network Topologies in Space. FPS@ETAPS 2014: 267-277 - [e3]Kenneth L. McMillan, Aart Middeldorp, Geoff Sutcliffe, Andrei Voronkov:
LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings. EPiC Series in Computing 26, EasyChair 2014 [contents] - [e2]Kenneth L. McMillan, Xavier Rival:
Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings. Lecture Notes in Computer Science 8318, Springer 2014, ISBN 978-3-642-54012-7 [contents] - 2013
- [c77]Aws Albarghouthi, Kenneth L. McMillan:
Beautiful Interpolants. CAV 2013: 313-329 - [c76]Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan:
Inductive invariant generation via abductive inference. OOPSLA 2013: 443-456 - [c75]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
On Solving Universally Quantified Horn Clauses. SAS 2013: 105-125 - [c74]Kenneth L. McMillan:
Deductive Generalization. SBMF 2013: 17 - [c73]Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, Chris Hawblitzel:
Differential assertion checking. ESEC/SIGSOFT FSE 2013: 345-355 - [c72]Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv:
Synthesis of Circular Compositional Program Proofs via Abduction. TACAS 2013: 370-384 - [e1]Kenneth L. McMillan, Aart Middeldorp, Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. Lecture Notes in Computer Science 8312, Springer 2013, ISBN 978-3-642-45220-8 [contents] - [i2]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. CoRR abs/1306.5264 (2013) - 2012
- [c71]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
Program Verification as Satisfiability Modulo Theories. SMT@IJCAR 2012: 3-11 - [c70]Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken:
Minimum Satisfying Assignments for SMT. CAV 2012: 394-409 - [c69]Thomas Ball, Nikolaj S. Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes:
Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. SPIN 2012: 1-6 - 2011
- [c68]Kenneth L. McMillan:
Interpolants from Z3 proofs. FMCAD 2011: 19-27 - [c67]Kenneth L. McMillan:
Widening and Interpolation. SAS 2011: 1 - [c66]Kenneth L. McMillan, Lenore D. Zuck:
Invisible Invariants and Abstract Interpretation. SAS 2011: 249-262 - 2010
- [c65]Kenneth L. McMillan:
Lazy Annotation for Program Testing and Verification. CAV 2010: 104-118
2000 – 2009
- 2009
- [c64]Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv:
Generalizing DPLL to Richer Logics. CAV 2009: 462-476 - [c63]Kenneth L. McMillan:
What's in Common between Test, Model Checking, and Decision Procedures? FMICS 2009: 35-36 - [c62]Kenneth L. McMillan, Lenore D. Zuck:
Abstract Counterexamples for Non-disjunctive Abstractions. RP 2009: 176-188 - 2008
- [j16]Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu:
Automated assumption generation for compositional verification. Formal Methods Syst. Des. 32(3): 285-301 (2008) - [c61]Kenneth L. McMillan:
Proofs, Interpolants, and Relevance Heuristics. Haifa Verification Conference 2008: 3 - [c60]Kenneth L. McMillan:
Relevance heuristics for program analysis. POPL 2008: 145-146 - [c59]Kenneth L. McMillan:
Quantified Invariant Generation Using an Interpolating Saturation Prover. TACAS 2008: 413-427 - 2007
- [j15]Ranjit Jhala, Kenneth L. McMillan:
Interpolant-Based Transition Relation Approximation. Log. Methods Comput. Sci. 3(4) (2007) - [c58]Kenneth L. McMillan:
Toward Property-Driven Abstraction for Heap Manipulating Programs. ATVA 2007: 17-18 - [c57]Ranjit Jhala, Kenneth L. McMillan:
Array Abstractions from Proofs. CAV 2007: 193-206 - [c56]Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu:
Automated Assumption Generation for Compositional Verification. CAV 2007: 420-432 - [c55]Nina Amla, Kenneth L. McMillan:
Combining Abstraction Refinement and SAT-Based Model Checking. TACAS 2007: 405-419 - [c54]Kenneth L. McMillan:
Interpolants and Symbolic Model Checking. VMCAI 2007: 89-90 - [i1]Ranjit Jhala, Kenneth L. McMillan:
Interpolant-Based Transition Relation Approximation. CoRR abs/0706.0523 (2007) - 2006
- [c53]Kenneth L. McMillan:
Lazy Abstraction with Interpolants. CAV 2006: 123-136 - [c52]Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck:
Liveness by Invisible Invariants. FORTE 2006: 356-371 - [c51]Ranjit Jhala, Kenneth L. McMillan:
A Practical and Complete Approach to Predicate Refinement. TACAS 2006: 459-473 - 2005
- [j14]Rajeev Alur, Kenneth L. McMillan, Doron A. Peled:
Deciding Global Partial-Order Properties. Formal Methods Syst. Des. 26(1): 7-25 (2005) - [j13]Kenneth L. McMillan:
An interpolating theorem prover. Theor. Comput. Sci. 345(1): 101-121 (2005) - [c50]Kenneth L. McMillan:
Applications of Craig Interpolation to Model Checking. ICATPN 2005: 15-16 - [c49]Ranjit Jhala, Kenneth L. McMillan:
Interpolant-Based Transition Relation Approximation. CAV 2005: 39-51 - [c48]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: 254-268 - [c47]Kenneth L. McMillan:
Applications of Craig Interpolants in Model Checking. TACAS 2005: 1-12 - 2004
- [c46]Kenneth L. McMillan:
Applications of Craig Interpolation to Model Checking. CSL 2004: 22-23 - [c45]Nina Amla, Kenneth L. McMillan:
A Hybrid of Counterexample-Based and Proof-Based Abstraction. FMCAD 2004: 260-274 - [c44]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan:
Abstractions from proofs. POPL 2004: 232-244 - [c43]Kenneth L. McMillan:
An Interpolating Theorem Prover. TACAS 2004: 16-30 - 2003
- [c42]Kenneth L. McMillan:
Interpolation and SAT-Based Model Checking. CAV 2003: 1-13 - [c41]Kenneth L. McMillan:
Methods for exploiting SAT solvers in unbounded model checking. MEMOCODE 2003: 135- - [c40]Kenneth L. McMillan:
Craig Interpolation and Reachability Analysis. SAS 2003: 336 - [c39]Kenneth L. McMillan, Nina Amla:
Automatic Abstraction without Counterexamples. TACAS 2003: 2-17 - [c38]Nina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo H. Medel:
Experimental Analysis of Different Techniques for Bounded Model Checking. TACAS 2003: 34-48 - 2002
- [c37]Kenneth L. McMillan:
Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002: 250-264 - 2001
- [j12]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): 1059-1076 (2001) - [c36]Ranjit Jhala, Kenneth L. McMillan:
Microarchitecture Verification by Compositional Model Checking. CAV 2001: 396-410 - [c35]Kenneth L. McMillan:
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. CHARME 2001: 179-195 - 2000
- [j11]Rajeev Alur, Kenneth L. McMillan, Doron A. Peled:
Model-Checking of Correctness Conditions for Concurrent Objects. Inf. Comput. 160(1-2): 167-188 (2000) - [j10]Kenneth L. McMillan:
A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37(1-3): 279-309 (2000) - [j9]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): 44-55 (2000) - [c34]Kenneth L. McMillan, Shaz Qadeer, James B. Saxe:
Induction in Compositional Model Checking. CAV 2000: 312-327 - [c33]Kenneth L. McMillan:
Some Strategies for Proving Theorems with a Model Checker. LICS 2000: 305-306
1990 – 1999
- 1999
- [c32]Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli:
Latency Insensitive Protocols. CAV 1999: 123-133 - [c31]Kenneth L. McMillan:
Verification of Infinite State Systems by Compositional Model Checking. CHARME 1999: 219-234 - [c30]Kenneth L. McMillan:
Circular Compositional Reasoning about Liveness. CHARME 1999: 342-345 - [c29]Luca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli:
A methodology for correct-by-construction latency insensitive design. ICCAD 1999: 309-315 - [c28]Andreas Kuehlmann, Kenneth L. McMillan, Robert K. Brayton:
Probabilistic state space search. ICCAD 1999: 574-579 - 1998
- [c27]Kenneth L. McMillan:
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. CAV 1998: 110-121 - [c26]Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi:
Approximation and Decomposition of Binary Decision Diagrams. DAC 1998: 445-450 - [c25]Kenneth L. McMillan:
Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract). FMCAD 1998: 1 - [c24]Kenneth L. McMillan:
Proof Rules for Model Checking Systems with Data. FSTTCS 1998: 270 - [c23]Rajeev Alur, Kenneth L. McMillan, Doron A. Peled:
Deciding Global Partial-Order Properties. ICALP 1998: 41-52 - 1997
- [j8]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): 137-148 (1997) - [c22]Kenneth L. McMillan:
A Compositional Rule for Hardware Design Refinement. CAV 1997: 24-35 - [c21]Youpyo Hong, Peter A. Beerel, Jerry R. Burch, Kenneth L. McMillan:
Safe BDD Minimization Using Don't Cares. DAC 1997: 208-213 - 1996
- [c20]Kenneth L. McMillan:
A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. CAV 1996: 13-25 - [c19]Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vasiliki Hartonas-Garmhausen:
Symbolic Model Checking. CAV 1996: 419-427 - [c18]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: 451-456 - [c17]Rajeev Alur, Kenneth L. McMillan, Doron A. Peled:
Model-Checking of Correctness Conditions for Concurrent Objects. LICS 1996: 219-228 - 1995
- [j7]Kenneth L. McMillan:
A Technique of State Space Search Based on Unfolding. Formal Methods Syst. Des. 6(1): 45-65 (1995) - [j6]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 Syst. Des. 6(2): 217-232 (1995) - [j5]Robert P. Kurshan, Kenneth L. McMillan:
A Structural Induction Theorem for Processes. Inf. Comput. 117(1): 1-11 (1995) - [c16]Kenneth L. McMillan:
Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. CAV 1995: 180-195 - [c15]Ásgeir Th. Eiríksson, Kenneth L. McMillan:
Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study. CAV 1995: 367-380 - [c14]Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao:
Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC 1995: 427-432 - [c13]Patrick C. McGeer, Kenneth L. McMillan, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli, Patrick Scaglia:
Fast discrete function evaluation using decision diagrams. ICCAD 1995: 402-407 - 1994
- [j4]Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, David L. Dill:
Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(4): 401-424 (1994) - [c12]Kenneth L. McMillan:
Hierarchical Representations of Discrete Functions, with Application to Model Checking. CAV 1994: 41-54 - [c11]Kenneth L. McMillan:
Fitting Formal Methods into the Design Cycle. DAC 1994: 314-319 - [c10]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: 320 - 1993
- [b1]Kenneth L. McMillan:
Symbolic model checking. Kluwer 1993, ISBN 978-0-7923-9380-1, pp. I-XV, 1-194 - [c9]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: