×

McMillan, Kenneth L.

Compute Distance To:
Author ID: mcmillan.kenneth-l Recent zbMATH articles by "McMillan, Kenneth L."
Published as: McMillan, Kenneth L.; McMillan, K. L.; McMillan, Ken; McMillan, Ken L.; McMillan, Kenneth

Publications by Year

Citations contained in zbMATH Open

40 Publications have been cited 833 times in 556 Documents Cited by Year
Symbolic model checking: \(10^{20}\) states and beyond. Zbl 0753.68066
Burch, J. R.; Clarke, E. M.; McMillan, K. L.; Dill, D. L.; Hwang, L. J.
156
1992
Interpolation and SAT-based model checking. Zbl 1278.68184
McMillan, K. L.
85
2003
Symbolic model checking. Foreword by Edmund Clarke. Zbl 0784.68004
McMillan, Kenneth L.
84
1993
Abstractions from proofs. Zbl 1325.68147
Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak; McMillan, Kenneth L.
54
2004
Lazy abstraction with interpolants. Zbl 1188.68196
McMillan, Kenneth L.
48
2006
An interpolating theorem prover. Zbl 1079.68092
McMillan, K. L.
37
2005
Interpolants and symbolic model checking. Zbl 1132.68474
McMillan, K. L.
36
2007
Horn clause solvers for program verification. Zbl 1465.68044
Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey
26
2015
Quantified invariant generation using an interpolating saturation prover. Zbl 1134.68416
McMillan, K. L.
25
2008
A practical and complete approach to predicate refinement. Zbl 1180.68118
Jhala, Ranjit; McMillan, K. L.
24
2006
A technique of state space search based on unfolding. Zbl 0829.68085
McMillan, K. L.
22
1995
Applying SAT methods in unbounded symbolic model checking. Zbl 1010.68509
McMillan, Ken L.
22
2002
Automatic abstraction without counterexamples. Zbl 1031.68520
McMillan, Kenneth L.; Amla, Nina
20
2003
Applications of Craig interpolants in model checking. Zbl 1087.68597
McMillan, K. L.
19
2005
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
19
1989
A structural induction theorem for processes. Zbl 0828.68096
Kurshan, R. P.; McMillan, K. L.
17
1995
Model-checking of correctness conditions for concurrent objects. Zbl 1003.68067
Alur, Rajeev; McMillan, Ken; Peled, Doron
16
2000
Interpolant-based transition relation approximation. Zbl 1081.68622
Jhala, Ranjit; McMillan, K. L.
15
2005
Array abstractions from proofs. Zbl 1135.68474
Jhala, Ranjit; McMillan, Kenneth L.
15
2007
An interpolating theorem prover. Zbl 1126.68573
McMillan, K. L.
13
2004
Synthesis of circular compositional program proofs via abduction. Zbl 1381.68057
Li, Boyang; Dillig, Isil; Dillig, Thomas; McMillan, Ken; Sagiv, Mooly
10
2013
Verification of finite state systems by compositional model checking. Zbl 0957.68068
McMillan, K. L.
9
1999
Generalizing DPLL to richer logics. Zbl 1242.68282
McMillan, Kenneth L.; Kuehlmann, Andreas; Sagiv, Mooly
8
2009
Parameterized verification of the FLASH cache coherence protocol by compositional model checking. Zbl 1002.68674
McMillan, K. L.
7
2001
Automated assumption generation for compositional verification. Zbl 1135.68473
Gupta, Anubhav; McMillan, Kenneth L.; Fu, Zhaohui
6
2007
Interpolation and model checking. Zbl 1392.68260
McMillan, Kenneth L.
5
2018
A methodology for hardware verification using compositional model checking. Zbl 0954.68005
McMillan, K. L.
4
2000
Microarchitecture verification by compositional model checking. Zbl 0991.68639
Jhala, Ranjit; McMillan, Kenneth L.
4
2001
Automated assumption generation for compositional verification. Zbl 1147.68050
Gupta, Anubhav; McMillan, K. L.; Fu, Zhaohui
4
2008
Induction in compositional model checking. Zbl 0974.68520
McMillan, Kenneth L.; Qadeer, Shaz; Saxe, James B.
3
2000
Latency insensitive protocols. Zbl 1046.68585
Carloni, Luca P.; McMillan, Kenneth L.; Sangiovanni-Vincentelli, Alberto L.
3
1999
Applications of Craig interpolation to model checking. Zbl 1095.68610
McMillan, Kenneth
3
2004
Interpolant-based transition relation approximation. Zbl 1131.68062
Jhala, Ranjit; McMillan, Kenneth L.
3
2007
Experimental analysis of different techniques for bounded model checking. Zbl 1031.68541
Amla, Nina; Kurshan, Robert; McMillan, Kenneth L.; Medel, Ricardo
2
2003
A hybrid of counterexample-based and proof-based abstraction. Zbl 1117.68420
Amla, Nina; McMillan, Ken L.
2
2004
An analysis of sAT-based model checking techniques in an industrial environment. Zbl 1159.68307
Amla, Nina; Du, Xiaoqun; Kuehlmann, Andreas; Kurshan, Robert P.; McMillan, Kenneth L.
2
2005
Combining abstraction refinement and SAT-based model checking. Zbl 1186.68274
Amla, Nina; McMillan, Kenneth L.
2
2007
Applications of Craig interpolation to model checking. Zbl 1128.68384
McMillan, Kenneth
1
2005
Liveness by invisible invariants. Zbl 1225.68114
Fang, Yi; McMillan, Kenneth L.; Pnueli, Amir; Zuck, Lenore D.
1
2006
Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Zbl 1277.68016
1
2013
Interpolation and model checking. Zbl 1392.68260
McMillan, Kenneth L.
5
2018
Horn clause solvers for program verification. Zbl 1465.68044
Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey
26
2015
Synthesis of circular compositional program proofs via abduction. Zbl 1381.68057
Li, Boyang; Dillig, Isil; Dillig, Thomas; McMillan, Ken; Sagiv, Mooly
10
2013
Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Zbl 1277.68016
1
2013
Generalizing DPLL to richer logics. Zbl 1242.68282
McMillan, Kenneth L.; Kuehlmann, Andreas; Sagiv, Mooly
8
2009
Quantified invariant generation using an interpolating saturation prover. Zbl 1134.68416
McMillan, K. L.
25
2008
Automated assumption generation for compositional verification. Zbl 1147.68050
Gupta, Anubhav; McMillan, K. L.; Fu, Zhaohui
4
2008
Interpolants and symbolic model checking. Zbl 1132.68474
McMillan, K. L.
36
2007
Array abstractions from proofs. Zbl 1135.68474
Jhala, Ranjit; McMillan, Kenneth L.
15
2007
Automated assumption generation for compositional verification. Zbl 1135.68473
Gupta, Anubhav; McMillan, Kenneth L.; Fu, Zhaohui
6
2007
Interpolant-based transition relation approximation. Zbl 1131.68062
Jhala, Ranjit; McMillan, Kenneth L.
3
2007
Combining abstraction refinement and SAT-based model checking. Zbl 1186.68274
Amla, Nina; McMillan, Kenneth L.
2
2007
Lazy abstraction with interpolants. Zbl 1188.68196
McMillan, Kenneth L.
48
2006
A practical and complete approach to predicate refinement. Zbl 1180.68118
Jhala, Ranjit; McMillan, K. L.
24
2006
Liveness by invisible invariants. Zbl 1225.68114
Fang, Yi; McMillan, Kenneth L.; Pnueli, Amir; Zuck, Lenore D.
1
2006
An interpolating theorem prover. Zbl 1079.68092
McMillan, K. L.
37
2005
Applications of Craig interpolants in model checking. Zbl 1087.68597
McMillan, K. L.
19
2005
Interpolant-based transition relation approximation. Zbl 1081.68622
Jhala, Ranjit; McMillan, K. L.
15
2005
An analysis of sAT-based model checking techniques in an industrial environment. Zbl 1159.68307
Amla, Nina; Du, Xiaoqun; Kuehlmann, Andreas; Kurshan, Robert P.; McMillan, Kenneth L.
2
2005
Applications of Craig interpolation to model checking. Zbl 1128.68384
McMillan, Kenneth
1
2005
Abstractions from proofs. Zbl 1325.68147
Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak; McMillan, Kenneth L.
54
2004
An interpolating theorem prover. Zbl 1126.68573
McMillan, K. L.
13
2004
Applications of Craig interpolation to model checking. Zbl 1095.68610
McMillan, Kenneth
3
2004
A hybrid of counterexample-based and proof-based abstraction. Zbl 1117.68420
Amla, Nina; McMillan, Ken L.
2
2004
Interpolation and SAT-based model checking. Zbl 1278.68184
McMillan, K. L.
85
2003
Automatic abstraction without counterexamples. Zbl 1031.68520
McMillan, Kenneth L.; Amla, Nina
20
2003
Experimental analysis of different techniques for bounded model checking. Zbl 1031.68541
Amla, Nina; Kurshan, Robert; McMillan, Kenneth L.; Medel, Ricardo
2
2003
Applying SAT methods in unbounded symbolic model checking. Zbl 1010.68509
McMillan, Ken L.
22
2002
Parameterized verification of the FLASH cache coherence protocol by compositional model checking. Zbl 1002.68674
McMillan, K. L.
7
2001
Microarchitecture verification by compositional model checking. Zbl 0991.68639
Jhala, Ranjit; McMillan, Kenneth L.
4
2001
Model-checking of correctness conditions for concurrent objects. Zbl 1003.68067
Alur, Rajeev; McMillan, Ken; Peled, Doron
16
2000
A methodology for hardware verification using compositional model checking. Zbl 0954.68005
McMillan, K. L.
4
2000
Induction in compositional model checking. Zbl 0974.68520
McMillan, Kenneth L.; Qadeer, Shaz; Saxe, James B.
3
2000
Verification of finite state systems by compositional model checking. Zbl 0957.68068
McMillan, K. L.
9
1999
Latency insensitive protocols. Zbl 1046.68585
Carloni, Luca P.; McMillan, Kenneth L.; Sangiovanni-Vincentelli, Alberto L.
3
1999
A technique of state space search based on unfolding. Zbl 0829.68085
McMillan, K. L.
22
1995
A structural induction theorem for processes. Zbl 0828.68096
Kurshan, R. P.; McMillan, K. L.
17
1995
Symbolic model checking. Foreword by Edmund Clarke. Zbl 0784.68004
McMillan, Kenneth L.
84
1993
Symbolic model checking: \(10^{20}\) states and beyond. Zbl 0753.68066
Burch, J. R.; Clarke, E. M.; McMillan, K. L.; Dill, D. L.; Hwang, L. J.
156
1992
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
19
1989
all top 5

Cited by 1,071 Authors

14 Vardi, Moshe Ya’akov
12 Kröning, Daniel
11 Grumberg, Orna
10 Ghilardi, Silvio
10 Rümmer, Philipp
9 Clarke, Edmund Melson jun.
8 Baldan, Paolo
8 Cimatti, Alessandro
8 Duan, Zhenhua
7 Henzinger, Thomas A.
7 Kapur, Deepak
7 McMillan, Kenneth L.
7 Pnueli, Amir
7 Rybalchenko, Andrey
7 Strichman, Ofer
6 Bouajjani, Ahmed
6 Corradini, Andrea
6 Gianola, Alessandro
6 Griggio, Alberto
6 Hoenicke, Jochen
6 Miller, Alice Ann
6 Podelski, Andreas
6 Santone, Antonella
6 Sharygina, Natasha
6 Tian, Cong
5 Enea, Constantin
5 Heljanko, Keijo
5 Kupferman, Orna
5 Roveri, Marco
5 Shoham, Sharon
5 Voronkov, Andrei
5 Weissenbacher, Georg
4 Biere, Armin
4 Bonacina, Maria Paola
4 Brillout, Angelo
4 Bruttomesso, Roberto
4 De Angelis, Emanuele
4 Dill, David L.
4 Droste, Manfred
4 Fedyukovich, Grigory
4 Fioravanti, Fabio
4 Gurfinkel, Arie
4 Kesten, Yonit
4 König, Barbara
4 Kulkarni, Sandeep S.
4 Kupferschmid, Stefan
4 Laroussinie, François
4 Malik, Sharad
4 Proietti, Maurizio
4 Ryvchin, Vadim
4 Schuppan, Viktor
4 Sebastiani, Roberto
4 Sofronie-Stokkermans, Viorica
4 Tinelli, Cesare
4 Tonetta, Stefano
4 Vojnar, Tomáš
4 Wahl, Thomas
4 Zhang, Nan
4 Zuck, Lenore D.
3 Abdulla, Parosh Aziz
3 Abujarad, Fuad
3 Bensalem, Saddek
3 Bloem, Roderick
3 Bonakdarpour, Borzoo
3 Brim, Luboš
3 Bryant, Randal E.
3 Bultan, Tevfik
3 Cabodi, Gianpiero
3 Calvanese, Diego
3 Chaki, Sagar
3 Chen, Mingshuai
3 Edelkamp, Stefan
3 Emmi, Michael
3 Gheorghe, Marian
3 Giunchiglia, Enrico
3 Gradara, Sara
3 Gupta, Aarti
3 Hélouët, Loïc
3 Heyman, Tamir
3 Huuck, Ralf
3 Johansson, Moa
3 Jovanović, Dejan
3 Kovács, Laura Ildikó
3 Kwiatkowska, Marta Z.
3 Lakhnech, Yassine
3 Lange, Martin
3 Lefticaru, Raluca
3 Lomuscio, Alessio
3 Lüttgen, Gerald
3 Madhusudan, Parthasarathy
3 Majumdar, Rupak
3 Majzik, Istvan
3 Marques-Silva, João P.
3 Montali, Marco
3 Olarte, Carlos
3 Ouaknine, Joel O.
3 Penczek, Wojciech
3 Pettorossi, Alberto
3 Pinna, G. Michele
3 Ranise, Silvio
...and 971 more Authors
all top 5

Cited in 73 Serials

64 Formal Methods in System Design
46 Theoretical Computer Science
28 Journal of Automated Reasoning
22 Information and Computation
18 Formal Aspects of Computing
16 Artificial Intelligence
15 Acta Informatica
9 Science of Computer Programming
7 Discrete Event Dynamic Systems
7 The Journal of Logic and Algebraic Programming
6 Journal of Computer and System Sciences
5 Discrete Applied Mathematics
5 Programming and Computer Software
5 Distributed Computing
5 Annals of Mathematics and Artificial Intelligence
5 Journal of Logical and Algebraic Methods in Programming
4 Information Processing Letters
4 Journal of Applied Mathematics
4 Journal of Applied Logic
3 Information Sciences
3 Synthese
3 Annals of Pure and Applied Logic
3 Journal of Symbolic Computation
3 MSCS. Mathematical Structures in Computer Science
3 Constraints
3 Theory and Practice of Logic Programming
3 ACM Transactions on Computational Logic
2 Journal of Computer Science and Technology
2 International Journal of Foundations of Computer Science
2 Cybernetics and Systems Analysis
2 Journal of Applied Non-Classical Logics
2 The Bulletin of Symbolic Logic
2 European Journal of Control
2 Computer Languages, Systems & Structures
2 Journal of Discrete Algorithms
2 Logical Methods in Computer Science
2 Science China. Information Sciences
1 Discrete Mathematics
1 International Journal of General Systems
1 Computing
1 Fuzzy Sets and Systems
1 Journal of Computational and Applied Mathematics
1 Journal of Mathematical Economics
1 Journal of Pure and Applied Algebra
1 Mathematics and Computers in Simulation
1 Studia Logica
1 Zeitschrift für Mathematische Logik und Grundlagen der Mathematik
1 Systems & Control Letters
1 International Journal of Production Research
1 Algorithmica
1 Linear Algebra and its Applications
1 RAIRO. Informatique Théorique et Applications
1 Russian Mathematics
1 Journal of Logic, Language and Information
1 Computational & Mathematical Organization Theory
1 International Transactions in Operational Research
1 Theory of Computing Systems
1 Wuhan University Journal of Natural Sciences (WUJNS)
1 Data Mining and Knowledge Discovery
1 Discrete Dynamics in Nature and Society
1 LMS Journal of Computation and Mathematics
1 International Journal of Applied Mathematics and Computer Science
1 Fundamenta Informaticae
1 Discrete Optimization
1 Science in China. Series F
1 Electronic Notes in Theoretical Computer Science
1 Logica Universalis
1 Journal of Satisfiability, Boolean Modeling and Computation
1 Algorithms
1 Asian Journal of Control
1 Frontiers of Computer Science in China
1 Computer Science Review
1 Journal of Membrane Computing

Citations by Year