×

zbMATH — the first resource for mathematics

McMillan, Kenneth L.

Compute Distance To:
Author ID: mcmillan.kenneth-l Recent zbMATH articles by "McMillan, Kenneth L."
Published as: McMillan, K. L.; McMillan, Ken; McMillan, Ken L.; McMillan, Kenneth; McMillan, Kenneth L.
Documents Indexed: 51 Publications since 1989, including 3 Books

Publications by Year

Citations contained in zbMATH Open

39 Publications have been cited 781 times in 495 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.
153
1992
Symbolic model checking. Foreword by Edmund Clarke. Zbl 0784.68004
McMillan, Kenneth L.
108
1993
Interpolation and SAT-based model checking. Zbl 1278.68184
McMillan, K. L.
80
2003
Abstractions from proofs. Zbl 1325.68147
Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak; McMillan, Kenneth L.
51
2004
Lazy abstraction with interpolants. Zbl 1188.68196
McMillan, Kenneth L.
41
2006
Interpolants and symbolic model checking. Zbl 1132.68474
McMillan, K. L.
35
2007
An interpolating theorem prover. Zbl 1079.68092
McMillan, K. L.
30
2005
A practical and complete approach to predicate refinement. Zbl 1180.68118
Jhala, Ranjit; McMillan, K. L.
21
2006
A technique of state space search based on unfolding. Zbl 0829.68085
McMillan, K. L.
21
1995
Quantified invariant generation using an interpolating saturation prover. Zbl 1134.68416
McMillan, K. L.
20
2008
Applying SAT methods in unbounded symbolic model checking. Zbl 1010.68509
McMillan, Ken L.
20
2002
Automatic abstraction without counterexamples. Zbl 1031.68520
McMillan, Kenneth L.; Amla, Nina
19
2003
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
19
1989
Applications of Craig interpolants in model checking. Zbl 1087.68597
McMillan, K. L.
18
2005
A structural induction theorem for processes. Zbl 0828.68096
Kurshan, R. P.; McMillan, K. L.
18
1995
Model-checking of correctness conditions for concurrent objects. Zbl 1003.68067
Alur, Rajeev; McMillan, Ken; Peled, Doron
16
2000
Array abstractions from proofs. Zbl 1135.68474
Jhala, Ranjit; McMillan, Kenneth L.
13
2007
Interpolant-based transition relation approximation. Zbl 1081.68622
Jhala, Ranjit; McMillan, K. L.
13
2005
An interpolating theorem prover. Zbl 1126.68573
McMillan, K. L.
10
2004
Verification of finite state systems by compositional model checking. Zbl 0957.68068
McMillan, K. L.
9
1999
Synthesis of circular compositional program proofs via abduction. Zbl 1381.68057
Li, Boyang; Dillig, Isil; Dillig, Thomas; McMillan, Ken; Sagiv, Mooly
7
2013
Horn clause solvers for program verification. Zbl 06484064
Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey
6
2015
Generalizing DPLL to richer logics. Zbl 1242.68282
McMillan, Kenneth L.; Kuehlmann, Andreas; Sagiv, Mooly
6
2009
Parameterized verification of the FLASH cache coherence protocol by compositional model checking. Zbl 1002.68674
McMillan, K. L.
6
2001
Automated assumption generation for compositional verification. Zbl 1135.68473
Gupta, Anubhav; McMillan, Kenneth L.; Fu, Zhaohui
5
2007
Interpolation and model checking. Zbl 1392.68260
McMillan, Kenneth L.
4
2018
Automated assumption generation for compositional verification. Zbl 1147.68050
Gupta, Anubhav; McMillan, K. L.; Fu, Zhaohui
4
2008
Microarchitecture verification by compositional model checking. Zbl 0991.68639
Jhala, Ranjit; McMillan, Kenneth L.
4
2001
Interpolant-based transition relation approximation. Zbl 1131.68062
Jhala, Ranjit; McMillan, Kenneth L.
3
2007
Induction in compositional model checking. Zbl 0974.68520
McMillan, Kenneth L.; Qadeer, Shaz; Saxe, James B.
3
2000
A methodology for hardware verification using compositional model checking. Zbl 0954.68005
McMillan, K. L.
3
2000
Latency insensitive protocols. Zbl 1046.68585
Carloni, Luca P.; McMillan, Kenneth L.; Sangiovanni-Vincentelli, Alberto L.
3
1999
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
A hybrid of counterexample-based and proof-based abstraction. Zbl 1117.68420
Amla, Nina; McMillan, Ken L.
2
2004
Applications of Craig interpolation to model checking. Zbl 1095.68610
McMillan, Kenneth
2
2004
Experimental analysis of different techniques for bounded model checking. Zbl 1031.68541
Amla, Nina; Kurshan, Robert; McMillan, Kenneth L.; Medel, Ricardo
2
2003
Applications of Craig interpolation to model checking. Zbl 1128.68384
McMillan, Kenneth
1
2005
Deciding global partial-order properties. Zbl 1075.68050
Alur, Rajeev; McMillan, Ken; Peled, Doron
1
2005
Interpolation and model checking. Zbl 1392.68260
McMillan, Kenneth L.
4
2018
Horn clause solvers for program verification. Zbl 06484064
Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey
6
2015
Synthesis of circular compositional program proofs via abduction. Zbl 1381.68057
Li, Boyang; Dillig, Isil; Dillig, Thomas; McMillan, Ken; Sagiv, Mooly
7
2013
Generalizing DPLL to richer logics. Zbl 1242.68282
McMillan, Kenneth L.; Kuehlmann, Andreas; Sagiv, Mooly
6
2009
Quantified invariant generation using an interpolating saturation prover. Zbl 1134.68416
McMillan, K. L.
20
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.
35
2007
Array abstractions from proofs. Zbl 1135.68474
Jhala, Ranjit; McMillan, Kenneth L.
13
2007
Automated assumption generation for compositional verification. Zbl 1135.68473
Gupta, Anubhav; McMillan, Kenneth L.; Fu, Zhaohui
5
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.
41
2006
A practical and complete approach to predicate refinement. Zbl 1180.68118
Jhala, Ranjit; McMillan, K. L.
21
2006
An interpolating theorem prover. Zbl 1079.68092
McMillan, K. L.
30
2005
Applications of Craig interpolants in model checking. Zbl 1087.68597
McMillan, K. L.
18
2005
Interpolant-based transition relation approximation. Zbl 1081.68622
Jhala, Ranjit; McMillan, K. L.
13
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
Deciding global partial-order properties. Zbl 1075.68050
Alur, Rajeev; McMillan, Ken; Peled, Doron
1
2005
Abstractions from proofs. Zbl 1325.68147
Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak; McMillan, Kenneth L.
51
2004
An interpolating theorem prover. Zbl 1126.68573
McMillan, K. L.
10
2004
A hybrid of counterexample-based and proof-based abstraction. Zbl 1117.68420
Amla, Nina; McMillan, Ken L.
2
2004
Applications of Craig interpolation to model checking. Zbl 1095.68610
McMillan, Kenneth
2
2004
Interpolation and SAT-based model checking. Zbl 1278.68184
McMillan, K. L.
80
2003
Automatic abstraction without counterexamples. Zbl 1031.68520
McMillan, Kenneth L.; Amla, Nina
19
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.
20
2002
Parameterized verification of the FLASH cache coherence protocol by compositional model checking. Zbl 1002.68674
McMillan, K. L.
6
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
Induction in compositional model checking. Zbl 0974.68520
McMillan, Kenneth L.; Qadeer, Shaz; Saxe, James B.
3
2000
A methodology for hardware verification using compositional model checking. Zbl 0954.68005
McMillan, K. L.
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.
21
1995
A structural induction theorem for processes. Zbl 0828.68096
Kurshan, R. P.; McMillan, K. L.
18
1995
Symbolic model checking. Foreword by Edmund Clarke. Zbl 0784.68004
McMillan, Kenneth L.
108
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.
153
1992
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
19
1989
all top 5

Cited by 990 Authors

14 Vardi, Moshe Y.
11 Grumberg, Orna
10 Kröning, Daniel
9 Clarke, Edmund Melson jun.
8 Baldan, Paolo
8 Cimatti, Alessandro
8 Duan, Zhenhua
7 Bouajjani, Ahmed
7 Henzinger, Thomas A.
7 Pnueli, Amir
6 Corradini, Andrea
6 Enea, Constantin
6 Ghilardi, Silvio
6 McMillan, Kenneth L.
6 Miller, Alice Ann
6 Rümmer, Philipp
6 Rybalchenko, Andrey
6 Santone, Antonella
6 Strichman, Ofer
6 Tian, Cong
5 Griggio, Alberto
5 Kupferman, Orna
5 Roveri, Marco
5 Sharygina, Natasha
5 Weissenbacher, Georg
4 Bruttomesso, Roberto
4 Dill, David L.
4 Emmi, Michael
4 Gurfinkel, Arie
4 Heljanko, Keijo
4 Hoenicke, Jochen
4 Kapur, Deepak
4 Kesten, Yonit
4 König, Barbara
4 Kulkarni, Sandeep S.
4 Kupferschmid, Stefan
4 Lomuscio, Alessio
4 Peled, Doron A.
4 Podelski, Andreas
4 Schuppan, Viktor
4 Sebastiani, Roberto
4 Shoham, Sharon
4 Tinelli, Cesare
4 Tonetta, Stefano
4 Vojnar, Tomáš
4 Voronkov, Andrei
4 Zhang, Nan
4 Zuck, Lenore D.
3 Abdulla, Parosh Aziz
3 Abujarad, Fuad
3 Alur, Rajeev
3 Bensalem, Saddek
3 Biere, Armin
3 Bloem, Roderick
3 Bonacina, Maria Paola
3 Bonakdarpour, Borzoo
3 Brillout, Angelo
3 Bultan, Tevfik
3 Cabodi, Gianpiero
3 Chaki, Sagar
3 Droste, Manfred
3 Edelkamp, Stefan
3 Giunchiglia, Enrico
3 Gradara, Sara
3 Hamza, Jad
3 Heyman, Tamir
3 Huuck, Ralf
3 Johansson, Moa
3 Konnov, Igor V.
3 Kwiatkowska, Marta Z.
3 Lakhnech, Yassine
3 Lange, Martin
3 Laroussinie, François
3 Lüttgen, Gerald
3 Madhusudan, Parthasarathy
3 Majumdar, Rupak
3 Malik, Sharad
3 Marques-Silva, João P.
3 Olarte, Carlos
3 Ouaknine, Joel O.
3 Penczek, Wojciech
3 Pinna, G. Michele
3 Ranise, Silvio
3 Ryvchin, Vadim
3 Schnoebelen, Ph
3 Schuster, Assaf
3 Sofronie-Stokkermans, Viorica
3 Song, Xiaoyu
3 Talpin, Jean-Pierre
3 Vaglini, Gigliola
3 Villani, Maria Luisa
3 Vizel, Yakir
3 Wahl, Thomas
3 Wang, Bow-Yaw
3 Zhang, Wenhui
2 Aiken, Alex
2 Alberti, Francesco
2 Baier, Christel
2 Becker, Bernd
2 Bertoli, Piergiorgio
...and 890 more Authors
all top 5

Cited in 69 Serials

59 Formal Methods in System Design
50 Theoretical Computer Science
24 Journal of Automated Reasoning
22 Information and Computation
18 Formal Aspects of Computing
17 Artificial Intelligence
13 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 Information Processing Letters
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 Journal of Applied Mathematics
4 Journal of Applied Logic
3 Information Sciences
3 Annals of Pure and Applied Logic
3 Journal of Symbolic Computation
3 MSCS. Mathematical Structures in Computer Science
3 Constraints
3 ACM Transactions on Computational Logic
2 Synthese
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 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 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 Theory and Practice of Logic Programming
1 Discrete Optimization
1 Science in China. Series F
1 Electronic Notes in Theoretical Computer Science
1 Logica Universalis
1 Logical Methods in Computer Science
1 Algorithms
1 Asian Journal of Control
1 Frontiers of Computer Science in China
1 Computer Science Review

Citations by Year