×

McMillan, Kenneth L.

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

45 Publications have been cited 1,088 times in 716 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.
200
1992
Symbolic model checking. Foreword by Edmund Clarke. Zbl 0784.68004
McMillan, Kenneth L.
126
1993
Interpolation and SAT-based model checking. Zbl 1278.68184
McMillan, K. L.
112
2003
Abstractions from proofs. Zbl 1325.68147
Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak; McMillan, Kenneth L.
67
2004
Lazy abstraction with interpolants. Zbl 1188.68196
McMillan, Kenneth L.
62
2006
Horn clause solvers for program verification. Zbl 1465.68044
Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey
49
2015
An interpolating theorem prover. Zbl 1079.68092
McMillan, K. L.
46
2005
Interpolants and symbolic model checking. Zbl 1132.68474
McMillan, K. L.
40
2007
Quantified invariant generation using an interpolating saturation prover. Zbl 1134.68416
McMillan, K. L.
30
2008
A practical and complete approach to predicate refinement. Zbl 1180.68118
Jhala, Ranjit; McMillan, K. L.
28
2006
A technique of state space search based on unfolding. Zbl 0829.68085
McMillan, K. L.
25
1995
Applying SAT methods in unbounded symbolic model checking. Zbl 1010.68509
McMillan, Ken L.
24
2002
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
24
1989
Applications of Craig interpolants in model checking. Zbl 1087.68597
McMillan, K. L.
23
2005
Automatic abstraction without counterexamples. Zbl 1031.68520
McMillan, Kenneth L.; Amla, Nina
22
2003
Synthesis of circular compositional program proofs via abduction. Zbl 1381.68057
Li, Boyang; Dillig, Isil; Dillig, Thomas; McMillan, Ken; Sagiv, Mooly
20
2013
A structural induction theorem for processes. Zbl 0828.68096
Kurshan, R. P.; McMillan, K. L.
19
1995
Array abstractions from proofs. Zbl 1135.68474
Jhala, Ranjit; McMillan, Kenneth L.
19
2007
Model-checking of correctness conditions for concurrent objects. Zbl 1003.68067
Alur, Rajeev; McMillan, Ken; Peled, Doron
17
2000
Interpolant-based transition relation approximation. Zbl 1081.68622
Jhala, Ranjit; McMillan, K. L.
17
2005
An interpolating theorem prover. Zbl 1126.68573
McMillan, K. L.
16
2004
Verification of finite state systems by compositional model checking. Zbl 0957.68068
McMillan, K. L.
12
1999
Parameterized verification of the FLASH cache coherence protocol by compositional model checking. Zbl 1002.68674
McMillan, K. L.
9
2001
Generalizing DPLL to richer logics. Zbl 1242.68282
McMillan, Kenneth L.; Kuehlmann, Andreas; Sagiv, Mooly
9
2009
Interpolation and model checking. Zbl 1392.68260
McMillan, Kenneth L.
7
2018
Automated assumption generation for compositional verification. Zbl 1135.68473
Gupta, Anubhav; McMillan, Kenneth L.; Fu, Zhaohui
7
2007
Automated assumption generation for compositional verification. Zbl 1147.68050
Gupta, Anubhav; McMillan, K. L.; Fu, Zhaohui
7
2008
A methodology for hardware verification using compositional model checking. Zbl 0954.68005
McMillan, K. L.
6
2000
Interpolant-based transition relation approximation. Zbl 1131.68062
Jhala, Ranjit; McMillan, Kenneth L.
5
2007
Induction in compositional model checking. Zbl 0974.68520
McMillan, Kenneth L.; Qadeer, Shaz; Saxe, James B.
4
2000
Microarchitecture verification by compositional model checking. Zbl 0991.68639
Jhala, Ranjit; McMillan, Kenneth L.
4
2001
Eager abstraction for symbolic model checking. Zbl 1511.68164
McMillan, Kenneth L.
4
2018
Deductive verification in decidable fragments with Ivy. Zbl 1511.68165
McMillan, Kenneth L.; Padon, Oded
4
2018
Applications of Craig interpolation to model checking. Zbl 1095.68610
McMillan, Kenneth
3
2004
Latency insensitive protocols. Zbl 1046.68585
Carloni, Luca P.; McMillan, Kenneth L.; Sangiovanni-Vincentelli, Alberto L.
3
1999
Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Zbl 1277.68016
3
2013
A hybrid of counterexample-based and proof-based abstraction. Zbl 1117.68420
Amla, Nina; McMillan, Ken L.
3
2004
Symbolic model checking. Zbl 0957.68062
McMillan, Kenneth L.
2
2000
Experimental analysis of different techniques for bounded model checking. Zbl 1031.68541
Amla, Nina; Kurshan, Robert; McMillan, Kenneth L.; Medel, Ricardo
2
2003
Combining abstraction refinement and SAT-based model checking. Zbl 1186.68274
Amla, Nina; McMillan, Kenneth L.
2
2007
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
Craig interpolation and reachability analysis. Zbl 1067.68580
McMillan, Ken L.
1
2003
Applications of Craig interpolation to model checking. Zbl 1128.68384
McMillan, Kenneth
1
2005
Temporal prophecy for proving temporal properties of infinite-state systems. Zbl 1522.68340
Padon, Oded; Hoenicke, Jochen; McMillan, Kenneth L.; Podelski, Andreas; Sagiv, Mooly; Shoham, Sharon
1
2021
Liveness by invisible invariants. Zbl 1225.68114
Fang, Yi; McMillan, Kenneth L.; Pnueli, Amir; Zuck, Lenore D.
1
2006
Temporal prophecy for proving temporal properties of infinite-state systems. Zbl 1522.68340
Padon, Oded; Hoenicke, Jochen; McMillan, Kenneth L.; Podelski, Andreas; Sagiv, Mooly; Shoham, Sharon
1
2021
Interpolation and model checking. Zbl 1392.68260
McMillan, Kenneth L.
7
2018
Eager abstraction for symbolic model checking. Zbl 1511.68164
McMillan, Kenneth L.
4
2018
Deductive verification in decidable fragments with Ivy. Zbl 1511.68165
McMillan, Kenneth L.; Padon, Oded
4
2018
Horn clause solvers for program verification. Zbl 1465.68044
Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey
49
2015
Synthesis of circular compositional program proofs via abduction. Zbl 1381.68057
Li, Boyang; Dillig, Isil; Dillig, Thomas; McMillan, Ken; Sagiv, Mooly
20
2013
Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Zbl 1277.68016
3
2013
Generalizing DPLL to richer logics. Zbl 1242.68282
McMillan, Kenneth L.; Kuehlmann, Andreas; Sagiv, Mooly
9
2009
Quantified invariant generation using an interpolating saturation prover. Zbl 1134.68416
McMillan, K. L.
30
2008
Automated assumption generation for compositional verification. Zbl 1147.68050
Gupta, Anubhav; McMillan, K. L.; Fu, Zhaohui
7
2008
Interpolants and symbolic model checking. Zbl 1132.68474
McMillan, K. L.
40
2007
Array abstractions from proofs. Zbl 1135.68474
Jhala, Ranjit; McMillan, Kenneth L.
19
2007
Automated assumption generation for compositional verification. Zbl 1135.68473
Gupta, Anubhav; McMillan, Kenneth L.; Fu, Zhaohui
7
2007
Interpolant-based transition relation approximation. Zbl 1131.68062
Jhala, Ranjit; McMillan, Kenneth L.
5
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.
62
2006
A practical and complete approach to predicate refinement. Zbl 1180.68118
Jhala, Ranjit; McMillan, K. L.
28
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.
46
2005
Applications of Craig interpolants in model checking. Zbl 1087.68597
McMillan, K. L.
23
2005
Interpolant-based transition relation approximation. Zbl 1081.68622
Jhala, Ranjit; McMillan, K. L.
17
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.
67
2004
An interpolating theorem prover. Zbl 1126.68573
McMillan, K. L.
16
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.
3
2004
Interpolation and SAT-based model checking. Zbl 1278.68184
McMillan, K. L.
112
2003
Automatic abstraction without counterexamples. Zbl 1031.68520
McMillan, Kenneth L.; Amla, Nina
22
2003
Experimental analysis of different techniques for bounded model checking. Zbl 1031.68541
Amla, Nina; Kurshan, Robert; McMillan, Kenneth L.; Medel, Ricardo
2
2003
Craig interpolation and reachability analysis. Zbl 1067.68580
McMillan, Ken L.
1
2003
Applying SAT methods in unbounded symbolic model checking. Zbl 1010.68509
McMillan, Ken L.
24
2002
Parameterized verification of the FLASH cache coherence protocol by compositional model checking. Zbl 1002.68674
McMillan, K. L.
9
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
17
2000
A methodology for hardware verification using compositional model checking. Zbl 0954.68005
McMillan, K. L.
6
2000
Induction in compositional model checking. Zbl 0974.68520
McMillan, Kenneth L.; Qadeer, Shaz; Saxe, James B.
4
2000
Symbolic model checking. Zbl 0957.68062
McMillan, Kenneth L.
2
2000
Verification of finite state systems by compositional model checking. Zbl 0957.68068
McMillan, K. L.
12
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.
25
1995
A structural induction theorem for processes. Zbl 0828.68096
Kurshan, R. P.; McMillan, K. L.
19
1995
Symbolic model checking. Foreword by Edmund Clarke. Zbl 0784.68004
McMillan, Kenneth L.
126
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.
200
1992
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
24
1989
all top 5

Cited by 1,317 Authors

17 Vardi, Moshe Ya’akov
15 Cimatti, Alessandro
14 Grumberg, Orna
13 Kröning, Daniel
12 Rümmer, Philipp
11 Clarke, Edmund Melson jun.
11 Duan, Zhenhua
11 Ghilardi, Silvio
10 Griggio, Alberto
9 Baldan, Paolo
9 Tian, Cong
8 De Angelis, Emanuele
8 Kapur, Deepak
8 McMillan, Kenneth L.
8 Shoham, Sharon
7 Bouajjani, Ahmed
7 Corradini, Andrea
7 Droste, Manfred
7 Fioravanti, Fabio
7 Gianola, Alessandro
7 Henzinger, Thomas A.
7 Hoenicke, Jochen
7 Pnueli, Amir
7 Proietti, Maurizio
7 Rybalchenko, Andrey
7 Sharygina, Natasha
7 Strichman, Ofer
7 Zhang, Nan
6 Abdulla, Parosh Aziz
6 Enea, Constantin
6 Fedyukovich, Grigory
6 Kobayashi, Naoki
6 König, Barbara
6 Kupferman, Orna
6 Miller, Alice Ann
6 Pettorossi, Alberto
6 Podelski, Andreas
6 Roveri, Marco
6 Santone, Antonella
6 Tonetta, Stefano
6 Weissenbacher, Georg
5 Biere, Armin
5 Bonacina, Maria Paola
5 Bryant, Randal E.
5 Gurfinkel, Arie
5 Heljanko, Keijo
5 Kovács, Laura Ildikó
5 Păsăreanu, Corina S.
5 Sebastiani, Roberto
5 Sofronie-Stokkermans, Viorica
5 Tinelli, Cesare
5 Voronkov, Andrei
4 Baier, Christel
4 Barrett, Clark W.
4 Brillout, Angelo
4 Bruttomesso, Roberto
4 Cabodi, Gianpiero
4 Chakraborty, Supratik
4 Dill, David L.
4 Emmi, Michael
4 Gupta, Aarti
4 Hermenegildo, Manuel V.
4 Holík, Lukáš
4 Kesten, Yonit
4 Kulkarni, Sandeep S.
4 Kupferschmid, Stefan
4 Kwiatkowska, Marta Z.
4 Laroussinie, François
4 Lomuscio, Alessio
4 Madhusudan, Parthasarathy
4 Majzik, Istvan
4 Malik, Sharad
4 Marques-Silva, João P.
4 Raskin, Jean-François
4 Ryvchin, Vadim
4 Sato, Ryosuke
4 Schuppan, Viktor
4 Song, Xiaoyu
4 Subramani, Krishnan
4 Vojnar, Tomáš
4 Wahl, Thomas
4 Wang, Bow-Yaw
4 Weidenbach, Christoph
4 Zuck, Lenore D.
3 Abujarad, Fuad
3 Bensalem, Saddek
3 Beyer, Dirk
3 Bloem, Roderick
3 Bonakdarpour, Borzoo
3 Bozzano, Marco
3 Brim, Luboš
3 Bromberger, Martin
3 Bultan, Tevfik
3 Calvanese, Diego
3 Chaki, Sagar
3 Chen, Mingshuai
3 Disch, Stefan
3 D’silva, Vijay
3 Edelkamp, Stefan
3 Fix, Limor
...and 1,217 more Authors
all top 5

Cited in 79 Serials

72 Formal Methods in System Design
50 Theoretical Computer Science
32 Journal of Automated Reasoning
23 Information and Computation
22 Formal Aspects of Computing
18 Artificial Intelligence
15 Acta Informatica
9 Science of Computer Programming
8 Discrete Event Dynamic Systems
8 The Journal of Logic and Algebraic Programming
8 Theory and Practice of Logic Programming
6 Journal of Computer and System Sciences
6 Annals of Mathematics and Artificial Intelligence
6 ACM Transactions on Computational Logic
6 Journal of Logical and Algebraic Methods in Programming
5 Discrete Applied Mathematics
5 Programming and Computer Software
5 Distributed Computing
5 Journal of Applied Logic
5 Logical Methods in Computer Science
4 Information Processing Letters
4 Information Sciences
4 Constraints
4 Journal of Applied Mathematics
3 Synthese
3 Annals of Pure and Applied Logic
3 Journal of Symbolic Computation
3 MSCS. Mathematical Structures in Computer Science
2 Journal of Computer Science and Technology
2 Machine Learning
2 International Journal of Foundations of Computer Science
2 Cybernetics and Systems Analysis
2 Journal of Logic, Language and Information
2 Journal of Applied Non-Classical Logics
2 The Bulletin of Symbolic Logic
2 European Journal of Control
2 Theory of Computing Systems
2 Computer Languages, Systems & Structures
2 Journal of Discrete Algorithms
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 International Journal of Approximate Reasoning
1 Linear Algebra and its Applications
1 RAIRO. Informatique Théorique et Applications
1 Russian Mathematics
1 Journal of Combinatorial Designs
1 Computational & Mathematical Organization Theory
1 International Transactions in Operational Research
1 Journal of Combinatorial Optimization
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 Journal of Zhejiang University. Science A
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 Journal of Theoretical Biology
1 Computer Science Review
1 Journal of Membrane Computing

Citations by Year