×

zbMATH — the first resource for mathematics

Klein, Gerwin

Compute Distance To:
Author ID: klein.gerwin Recent zbMATH articles by "Klein, Gerwin"
Published as: Klein, Gerwin; Klein, G.
Documents Indexed: 40 Publications since 1952, including 2 Books

Publications by Year

Citations contained in zbMATH Open

31 Publications have been cited 169 times in 97 Documents Cited by Year
Concrete semantics. With Isabelle/HOL. Zbl 1410.68004
Nipkow, Tobias; Klein, Gerwin
31
2014
Eigenvalue-generalized eigenvector assignment with state feedback. Zbl 0346.93020
Klein, G.; Moore, B. C.
22
1977
Types, bytes, and separation logic. Zbl 1295.68094
Tuch, Harvey; Klein, Gerwin; Norrish, Michael
21
2007
Verified bytecode verifiers. Zbl 1038.68109
Klein, Gerwin; Nipkow, Tobias
15
2003
Operating system verification—an overview. Zbl 1192.68432
Klein, Gerwin
13
2009
Secure microkernels, state monads and scalable refinement. Zbl 1165.68454
Cock, David; Klein, Gerwin; Sewell, Thomas
8
2008
Verified lightweight bytecode verification. Zbl 0997.68018
Klein, Gerwin; Nipkow, Tobias
5
2001
Bridging the gap: automatic verified abstraction of C. Zbl 1360.68751
Greenaway, David; Andronick, June; Klein, Gerwin
5
2012
On spline functions and statistical regularization of ill-posed problems. Zbl 0439.65107
Klein, G.
4
1979
A unified memory model for pointers. Zbl 1143.68464
Tuch, Harvey; Klein, Gerwin
4
2005
Newtonian trajectories and quantum waves in expanding force fields. Zbl 0617.70014
Berry, M. V.; Klein, G.
4
1984
Noninterference for operating system kernels. Zbl 1383.68021
Murray, Toby; Matichuk, Daniel; Brassil, Matthew; Gammie, Peter; Klein, Gerwin
4
2012
Sur la mécanique statistique des phénomènes irréversibles. I. II. Zbl 0050.20404
Klein, G.; Prigogine, I.
3
1953
A contribution to flame theory. Zbl 0078.22106
Klein, G.
3
1957
Verified bytecode subroutines. Zbl 1031.68040
Klein, G.; Wildmoser, M.
3
2003
Refinement through restraint: bringing down the cost of verification. Zbl 1361.68045
O’Connor, Liam; Chen, Zilin; Rizkallah, Christine; Amani, Sidney; Lim, Japheth; Murray, Toby; Nagashima, Yutaka; Sewell, Thomas; Klein, Gerwin
3
2016
Prototyping proof carrying code. Zbl 1094.68015
Wildmoser, Martin; Nipkow, Tobias; Klein, Gerwin; Nanz, Sebastian
2
2004
Mean first-passage times of Brownian motion and related problems. Zbl 0049.26203
Klein, G.
2
1952
A generalization of the classical random-walk problem and a simple model of Brownian motion based theorem. Zbl 0049.26204
Klein, G.
2
1952
Types, maps and separation logic. Zbl 1252.03079
Kolanski, Rafal; Klein, Gerwin
2
2009
Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Zbl 1294.68020
Klein, Gerwin (ed.); Gamboa, Ruben (ed.)
2
2014
Mechanised separation algebra. Zbl 1360.68754
Klein, Gerwin; Kolanski, Rafal; Boyton, Andrew
2
2012
Program verification in the presence of cached address translation. Zbl 06947001
Syeda, Hira Taqdees; Klein, Gerwin
1
2018
Reasoning about translation lookaside buffers. Zbl 1403.68037
Taqdees, Syeda Hira; Klein, Gerwin
1
2017
Verified bytecode verification and type-certifying compilation. Zbl 1067.68039
Klein, Gerwin; Strecker, Martin
1
2004
Sur la mécanique statistique des phénomènes irréversibles. III. Zbl 0051.42704
Klein, G.; Prigogine, I.
1
1953
Der Einfluß der Abänderung von Elementen einer Matrix auf ihre inverse Matrix. Zbl 0173.44202
Klein, G.
1
1964
Experience report: seL4, formally verifying a high-performance microkernel. Zbl 1302.68090
Klein, Gerwin; Derrin, Philip; Elphinstone, Kevin
1
2009
Challenges and experiences in managing large-scale proofs. Zbl 1359.68264
Bourke, Timothy; Daum, Matthias; Klein, Gerwin; Kolanski, Rafal
1
2012
seL4 enforces integrity. Zbl 1342.68303
Sewell, Thomas; Winwood, Simon; Gammie, Peter; Murray, Toby; Andronick, June; Klein, Gerwin
1
2011
Concerned with the unprivileged: user programs in kernel refinement. Zbl 1342.68079
Daum, Matthias; Billing, Nelson; Klein, Gerwin
1
2014
Program verification in the presence of cached address translation. Zbl 06947001
Syeda, Hira Taqdees; Klein, Gerwin
1
2018
Reasoning about translation lookaside buffers. Zbl 1403.68037
Taqdees, Syeda Hira; Klein, Gerwin
1
2017
Refinement through restraint: bringing down the cost of verification. Zbl 1361.68045
O’Connor, Liam; Chen, Zilin; Rizkallah, Christine; Amani, Sidney; Lim, Japheth; Murray, Toby; Nagashima, Yutaka; Sewell, Thomas; Klein, Gerwin
3
2016
Concrete semantics. With Isabelle/HOL. Zbl 1410.68004
Nipkow, Tobias; Klein, Gerwin
31
2014
Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Zbl 1294.68020
Klein, Gerwin; Gamboa, Ruben
2
2014
Concerned with the unprivileged: user programs in kernel refinement. Zbl 1342.68079
Daum, Matthias; Billing, Nelson; Klein, Gerwin
1
2014
Bridging the gap: automatic verified abstraction of C. Zbl 1360.68751
Greenaway, David; Andronick, June; Klein, Gerwin
5
2012
Noninterference for operating system kernels. Zbl 1383.68021
Murray, Toby; Matichuk, Daniel; Brassil, Matthew; Gammie, Peter; Klein, Gerwin
4
2012
Mechanised separation algebra. Zbl 1360.68754
Klein, Gerwin; Kolanski, Rafal; Boyton, Andrew
2
2012
Challenges and experiences in managing large-scale proofs. Zbl 1359.68264
Bourke, Timothy; Daum, Matthias; Klein, Gerwin; Kolanski, Rafal
1
2012
seL4 enforces integrity. Zbl 1342.68303
Sewell, Thomas; Winwood, Simon; Gammie, Peter; Murray, Toby; Andronick, June; Klein, Gerwin
1
2011
Operating system verification—an overview. Zbl 1192.68432
Klein, Gerwin
13
2009
Types, maps and separation logic. Zbl 1252.03079
Kolanski, Rafal; Klein, Gerwin
2
2009
Experience report: seL4, formally verifying a high-performance microkernel. Zbl 1302.68090
Klein, Gerwin; Derrin, Philip; Elphinstone, Kevin
1
2009
Secure microkernels, state monads and scalable refinement. Zbl 1165.68454
Cock, David; Klein, Gerwin; Sewell, Thomas
8
2008
Types, bytes, and separation logic. Zbl 1295.68094
Tuch, Harvey; Klein, Gerwin; Norrish, Michael
21
2007
A unified memory model for pointers. Zbl 1143.68464
Tuch, Harvey; Klein, Gerwin
4
2005
Prototyping proof carrying code. Zbl 1094.68015
Wildmoser, Martin; Nipkow, Tobias; Klein, Gerwin; Nanz, Sebastian
2
2004
Verified bytecode verification and type-certifying compilation. Zbl 1067.68039
Klein, Gerwin; Strecker, Martin
1
2004
Verified bytecode verifiers. Zbl 1038.68109
Klein, Gerwin; Nipkow, Tobias
15
2003
Verified bytecode subroutines. Zbl 1031.68040
Klein, G.; Wildmoser, M.
3
2003
Verified lightweight bytecode verification. Zbl 0997.68018
Klein, Gerwin; Nipkow, Tobias
5
2001
Newtonian trajectories and quantum waves in expanding force fields. Zbl 0617.70014
Berry, M. V.; Klein, G.
4
1984
On spline functions and statistical regularization of ill-posed problems. Zbl 0439.65107
Klein, G.
4
1979
Eigenvalue-generalized eigenvector assignment with state feedback. Zbl 0346.93020
Klein, G.; Moore, B. C.
22
1977
Der Einfluß der Abänderung von Elementen einer Matrix auf ihre inverse Matrix. Zbl 0173.44202
Klein, G.
1
1964
A contribution to flame theory. Zbl 0078.22106
Klein, G.
3
1957
Sur la mécanique statistique des phénomènes irréversibles. I. II. Zbl 0050.20404
Klein, G.; Prigogine, I.
3
1953
Sur la mécanique statistique des phénomènes irréversibles. III. Zbl 0051.42704
Klein, G.; Prigogine, I.
1
1953
Mean first-passage times of Brownian motion and related problems. Zbl 0049.26203
Klein, G.
2
1952
A generalization of the classical random-walk problem and a simple model of Brownian motion based theorem. Zbl 0049.26204
Klein, G.
2
1952
all top 5

Cited by 185 Authors

9 Klein, Gerwin
8 Blanchette, Jasmin Christian
7 Nipkow, Tobias
5 Lammich, Peter
5 Popescu, Andrei
4 Lochbihler, Andreas
4 Myreen, Magnus O.
4 Paulson, Lawrence Charles
4 Pichardie, David
3 Barthe, Gilles
3 Besson, Frédéric
3 Kumar, Ramana
3 Murray, Toby
3 Sefidgar, S. Reza
3 Sewell, Thomas D.
3 Traytel, Dmitry
3 Wenzel, Makarius
3 Wolff, Burkhart
2 Alkassar, Eyad
2 Andronick, June
2 Arthan, Rob D.
2 Asperti, Andrea
2 Bauereiß, Thomas
2 Blazy, Sandrine
2 Böhme, Sascha
2 Cachera, David
2 Daum, Matthias
2 Fleury, Mathias
2 Guttmann, Walter
2 Haslbeck, Max W.
2 Haslbeck, Maximilian P. L.
2 Hupel, Lars
2 Matichuk, Daniel
2 Norrish, Michael
2 Owens, Scott
2 Peña, Ricardo
2 Pesenti Gritti, Armando
2 Raimondi, Franco
2 Rizkallah, Christine
2 Schlichtkrull, Anders
2 Strecker, Martin
2 Weidenbach, Christoph
2 Woodcock, James C. P.
1 Albert, Elvira
1 Arenas, Puri
1 Aspinall, David
1 Avigad, Jeremy
1 Bach Poulsen, Casper
1 Basin, David A.
1 Basu, Amitabh
1 Bentkamp, Alexander
1 Beringer, Lennart
1 Betarte, Gustavo
1 Billing, Nelson
1 Bottesch, Ralph Christian
1 Bringsjord, Selmer
1 Brinkop, Hauke
1 Brucker, Achim D.
1 Bulwahn, Lukas
1 Campo, Juan Diego
1 Carle, Georg
1 Chen, Zilin
1 Cheng, Shu
1 Chlipala, Adam J.
1 Ciaffaglione, Alberto
1 Cock, David
1 Courtieu, Pierre
1 Crespo, Juan Manuel
1 de Dios, Javier
1 Derrick, John
1 Diekmann, Cornelius
1 Divasón, Jose
1 Doherty, Simon
1 Dong, JinSong
1 Dongol, Brijesh
1 Dörrenbächer, Jan
1 D’Souza, Deepak
1 Dufay, Guillaume
1 Eberl, Manuel
1 Echenim, Mnacho
1 Eggert, Sebastian
1 Erkök, Levent
1 Ford, Ian J.
1 Fox, Anthony C. J.
1 Gammie, Peter
1 Gascón, Adrià
1 Gast, Holger
1 Geuvers, Jan Herman
1 Gheri, Lorenzo
1 Giorgino, Mathieu
1 Gordon, Michael J. C.
1 Greenaway, David
1 Groce, Alex
1 Guéneau, Armaël
1 Guiol, Hervé
1 Haftmann, Florian
1 Havelund, Klaus
1 Hermenegildo, Manuel V.
1 Hillebrand, Mark A.
1 Hoa, Koh Chuen
...and 85 more Authors

Citations by Year