default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Gerwin Klein
@article{DBLP:journals/afp/BrecknellGHIKKLNSSSTW24,
author = {Matthew Brecknell and
David Greenaway and
Johannes H{\"{o}}lzl and
Fabian Immler and
Gerwin Klein and
Rafal Kolanski and
Japheth Lim and
Michael Norrish and
Norbert Schirmer and
Salomon Sickert and
Thomas Sewell and
Harvey Tuch and
Simon Wimmer},
title = {AutoCorres2},
journal = {Arch. Formal Proofs},
volume = {2024},
year = {2024},
url = {https://www.isa-afp.org/entries/AutoCorres2.html},
timestamp = {Mon, 29 Jul 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/BrecknellGHIKKLNSSSTW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fm/SisonBMKH23,
author = {Robert Sison and
Scott Buckley and
Toby Murray and
Gerwin Klein and
Gernot Heiser},
editor = {Marsha Chechik and
Joost{-}Pieter Katoen and
Martin Leucker},
title = {Formalising the Prevention of Microarchitectural Timing Channels by
Operating Systems},
booktitle = {Formal Methods - 25th International Symposium, {FM} 2023, L{\"{u}}beck,
Germany, March 6-10, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14000},
pages = {103--121},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-27481-7\_8},
doi = {10.1007/978-3-031-27481-7\_8},
timestamp = {Sat, 11 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/fm/SisonBMKH23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2310-17046,
author = {Scott Buckley and
Robert Sison and
Nils Wistoff and
Curtis Millar and
Toby Murray and
Gerwin Klein and
Gernot Heiser},
title = {Proving the Absence of Microarchitectural Timing Channels},
journal = {CoRR},
volume = {abs/2310.17046},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2310.17046},
doi = {10.48550/ARXIV.2310.17046},
eprinttype = {arXiv},
eprint = {2310.17046},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2310-17046.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ieeesp/CoferABHSAHRKLM22,
author = {Darren D. Cofer and
Isaac Amundson and
Junaid Babar and
David S. Hardin and
Konrad Slind and
Perry Alexander and
John Hatcliff and
Robby and
Gerwin Klein and
Corey Lewis and
Eric Mercer and
John Shackleton},
title = {Cyberassured Systems Engineering at Scale},
journal = {{IEEE} Secur. Priv.},
volume = {20},
number = {3},
pages = {52--64},
year = {2022},
url = {https://doi.org/10.1109/MSEC.2022.3151733},
doi = {10.1109/MSEC.2022.3151733},
timestamp = {Mon, 13 Jun 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/ieeesp/CoferABHSAHRKLM22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sle/ChenROSKHK22,
author = {Zilin Chen and
Christine Rizkallah and
Liam O'Connor and
Partha Susarla and
Gerwin Klein and
Gernot Heiser and
Gabriele Keller},
editor = {Bernd Fischer and
Lola Burgue{\~{n}}o and
Walter Cazzola},
title = {Property-Based Testing: Climbing the Stairway to Verification},
booktitle = {Proceedings of the 15th {ACM} {SIGPLAN} International Conference on
Software Language Engineering, {SLE} 2022, Auckland, New Zealand,
December 6-7, 2022},
pages = {84--97},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3567512.3567520},
doi = {10.1145/3567512.3567520},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/sle/ChenROSKHK22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfp/OConnorCRJAKMSK21,
author = {Liam O'Connor and
Zilin Chen and
Christine Rizkallah and
Vincent Jackson and
Sidney Amani and
Gerwin Klein and
Toby Murray and
Thomas Sewell and
Gabriele Keller},
title = {Cogent: uniqueness types and certifying compilation},
journal = {J. Funct. Program.},
volume = {31},
pages = {e25},
year = {2021},
url = {https://doi.org/10.1017/S095679682100023X},
doi = {10.1017/S095679682100023X},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfp/OConnorCRJAKMSK21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cacm/HeiserKA20,
author = {Gernot Heiser and
Gerwin Klein and
June Andronick},
title = {seL4 in Australia: from research to real-world trustworthy systems},
journal = {Commun. {ACM}},
volume = {63},
number = {4},
pages = {72--75},
year = {2020},
url = {https://doi.org/10.1145/3378426},
doi = {10.1145/3378426},
timestamp = {Fri, 17 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/cacm/HeiserKA20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/SyedaK20,
author = {Hira Taqdees Syeda and
Gerwin Klein},
title = {Formal Reasoning Under Cached Address Translation},
journal = {J. Autom. Reason.},
volume = {64},
number = {5},
pages = {911--945},
year = {2020},
url = {https://doi.org/10.1007/s10817-019-09539-7},
doi = {10.1007/S10817-019-09539-7},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/SyedaK20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sigops/HeiserMK20,
author = {Gernot Heiser and
Toby Murray and
Gerwin Klein},
title = {Towards Provable Timing-Channel Prevention},
journal = {{ACM} {SIGOPS} Oper. Syst. Rev.},
volume = {54},
number = {1},
pages = {1--7},
year = {2020},
url = {https://doi.org/10.1145/3421473.3421475},
doi = {10.1145/3421473.3421475},
timestamp = {Tue, 06 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sigops/HeiserMK20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/hotos/HeiserKM19,
author = {Gernot Heiser and
Gerwin Klein and
Toby C. Murray},
title = {Can We Prove Time Protection?},
booktitle = {Proceedings of the Workshop on Hot Topics in Operating Systems, HotOS
2019, Bertinoro, Italy, May 13-15, 2019},
pages = {23--29},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3317550.3321431},
doi = {10.1145/3317550.3321431},
timestamp = {Wed, 29 May 2019 13:38:37 +0200},
biburl = {https://dblp.org/rec/conf/hotos/HeiserKM19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1901-08338,
author = {Gernot Heiser and
Gerwin Klein and
Toby C. Murray},
title = {Can We Prove Time Protection?},
journal = {CoRR},
volume = {abs/1901.08338},
year = {2019},
url = {http://arxiv.org/abs/1901.08338},
eprinttype = {arXiv},
eprint = {1901.08338},
timestamp = {Sat, 02 Feb 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1901-08338.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cacm/KleinAFKMH18,
author = {Gerwin Klein and
June Andronick and
Matthew Fernandez and
Ihor Kuz and
Toby C. Murray and
Gernot Heiser},
title = {Formally verified software in the real world},
journal = {Commun. {ACM}},
volume = {61},
number = {10},
pages = {68--77},
year = {2018},
url = {https://doi.org/10.1145/3230627},
doi = {10.1145/3230627},
timestamp = {Sun, 02 Jun 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/cacm/KleinAFKMH18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/computer/CoferGBWPFPKKAH18,
author = {Darren D. Cofer and
Andrew Gacek and
John Backes and
Michael W. Whalen and
Lee Pike and
Adam Foltzer and
Michal Podhradsky and
Gerwin Klein and
Ihor Kuz and
June Andronick and
Gernot Heiser and
Douglas Stuart},
title = {A Formal Approach to Constructing Secure Air Vehicle Software},
journal = {Computer},
volume = {51},
number = {11},
pages = {14--23},
year = {2018},
url = {https://doi.org/10.1109/MC.2018.2876051},
doi = {10.1109/MC.2018.2876051},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/computer/CoferGBWPFPKKAH18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/AvigadBKPPS18,
author = {Jeremy Avigad and
Jasmin Christian Blanchette and
Gerwin Klein and
Lawrence C. Paulson and
Andrei Popescu and
Gregor Snelting},
title = {Introduction to Milestones in Interactive Theorem Proving},
journal = {J. Autom. Reason.},
volume = {61},
number = {1-4},
pages = {1--8},
year = {2018},
url = {https://doi.org/10.1007/s10817-018-9465-5},
doi = {10.1007/S10817-018-9465-5},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/AvigadBKPPS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/isola/OConnorCSRKK18,
author = {Liam O'Connor and
Zilin Chen and
Partha Susarla and
Christine Rizkallah and
Gerwin Klein and
Gabriele Keller},
editor = {Tiziana Margaria and
Bernhard Steffen},
title = {Bringing Effortless Refinement of Data Layouts to Cogent},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation.
Modeling - 8th International Symposium, ISoLA 2018, Limassol, Cyprus,
November 5-9, 2018, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {11244},
pages = {134--149},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-030-03418-4\_9},
doi = {10.1007/978-3-030-03418-4\_9},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/isola/OConnorCSRKK18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BannisterHK18,
author = {Callum Bannister and
Peter H{\"{o}}fner and
Gerwin Klein},
editor = {Jeremy Avigad and
Assia Mahboubi},
title = {Backwards and Forwards with Separation Logic},
booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 9-12, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10895},
pages = {68--87},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94821-8\_5},
doi = {10.1007/978-3-319-94821-8\_5},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/BannisterHK18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/SyedaK18,
author = {Hira Taqdees Syeda and
Gerwin Klein},
editor = {Jeremy Avigad and
Assia Mahboubi},
title = {Program Verification in the Presence of Cached Address Translation},
booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 9-12, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10895},
pages = {542--559},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94821-8\_32},
doi = {10.1007/978-3-319-94821-8\_32},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/SyedaK18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/SyedaK17,
author = {Hira Taqdees Syeda and
Gerwin Klein},
editor = {Thomas Eiter and
David Sands},
title = {Reasoning about Translation Lookaside Buffers},
booktitle = {LPAR-21, 21st International Conference on Logic for Programming, Artificial
Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017},
series = {EPiC Series in Computing},
volume = {46},
pages = {490--508},
publisher = {EasyChair},
year = {2017},
url = {https://doi.org/10.29007/c2f1},
doi = {10.29007/C2F1},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/SyedaK17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sosp/ChenOKKH17,
author = {Zilin Chen and
Liam O'Connor and
Gabriele Keller and
Gerwin Klein and
Gernot Heiser},
editor = {Julia Lawall},
title = {The Cogent Case for Property-Based Testing},
booktitle = {Proceedings of the 9th Workshop on Programming Languages and Operating
Systems, Shanghai, China, October 28, 2017},
pages = {1--7},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3144555.3144556},
doi = {10.1145/3144555.3144556},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/sosp/ChenOKKH17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/BeerenFGKKLLMS16,
author = {Joel Beeren and
Matthew Fernandez and
Xin Gao and
Gerwin Klein and
Rafal Kolanski and
Japheth Lim and
Corey Lewis and
Daniel Matichuk and
Thomas Sewell},
title = {Finite Machine Word Library},
journal = {Arch. Formal Proofs},
volume = {2016},
year = {2016},
url = {https://www.isa-afp.org/entries/Word\_Lib.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/BeerenFGKKLLMS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/KleinG16,
author = {Gerwin Klein and
Ruben Gamboa},
title = {Interactive Theorem Proving - Preface of the Special Issue},
journal = {J. Autom. Reason.},
volume = {56},
number = {3},
pages = {201--203},
year = {2016},
url = {https://doi.org/10.1007/s10817-016-9363-7},
doi = {10.1007/S10817-016-9363-7},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/KleinG16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/asplos/AmaniHCRCOBNLST16,
author = {Sidney Amani and
Alex Hixon and
Zilin Chen and
Christine Rizkallah and
Peter Chubb and
Liam O'Connor and
Joel Beeren and
Yutaka Nagashima and
Japheth Lim and
Thomas Sewell and
Joseph Tuong and
Gabriele Keller and
Toby C. Murray and
Gerwin Klein and
Gernot Heiser},
editor = {Tom Conte and
Yuanyuan Zhou},
title = {CoGENT: Verifying High-Assurance File System Implementations},
booktitle = {Proceedings of the Twenty-First International Conference on Architectural
Support for Programming Languages and Operating Systems, {ASPLOS}
2016, Atlanta, GA, USA, April 2-6, 2016},
pages = {175--188},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2872362.2872404},
doi = {10.1145/2872362.2872404},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/asplos/AmaniHCRCOBNLST16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/OConnorCRALMNSK16,
author = {Liam O'Connor and
Zilin Chen and
Christine Rizkallah and
Sidney Amani and
Japheth Lim and
Toby C. Murray and
Yutaka Nagashima and
Thomas Sewell and
Gerwin Klein},
editor = {Jacques Garrigue and
Gabriele Keller and
Eijiro Sumii},
title = {Refinement through restraint: bringing down the cost of verification},
booktitle = {Proceedings of the 21st {ACM} {SIGPLAN} International Conference on
Functional Programming, {ICFP} 2016, Nara, Japan, September 18-22,
2016},
pages = {89--102},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2951913.2951940},
doi = {10.1145/2951913.2951940},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/icfp/OConnorCRALMNSK16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/RizkallahLNSCOM16,
author = {Christine Rizkallah and
Japheth Lim and
Yutaka Nagashima and
Thomas Sewell and
Zilin Chen and
Liam O'Connor and
Toby C. Murray and
Gabriele Keller and
Gerwin Klein},
editor = {Jasmin Christian Blanchette and
Stephan Merz},
title = {A Framework for the Automatic Formal Verification of Refinement from {C}ogent to C.},
booktitle = {Interactive Theorem Proving - 7th International Conference, {ITP}
2016, Nancy, France, August 22-25, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9807},
pages = {323--340},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-43144-4\_20},
doi = {10.1007/978-3-319-43144-4\_20},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/itp/RizkallahLNSCOM16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/OConnorRCALNSHK16,
author = {Liam O'Connor and
Christine Rizkallah and
Zilin Chen and
Sidney Amani and
Japheth Lim and
Yutaka Nagashima and
Thomas Sewell and
Alex Hixon and
Gabriele Keller and
Toby C. Murray and
Gerwin Klein},
title = {{COGENT:} Certified Compilation for a Functional Systems Language},
journal = {CoRR},
volume = {abs/1601.05520},
year = {2016},
url = {http://arxiv.org/abs/1601.05520},
eprinttype = {arXiv},
eprint = {1601.05520},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/OConnorRCALNSHK16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/infsof/JefferySAKM15,
author = {D. Ross Jeffery and
Mark Staples and
June Andronick and
Gerwin Klein and
Toby C. Murray},
title = {An empirical research agenda for understanding formal methods productivity},
journal = {Inf. Softw. Technol.},
volume = {60},
pages = {102--112},
year = {2015},
url = {https://doi.org/10.1016/j.infsof.2014.11.005},
doi = {10.1016/J.INFSOF.2014.11.005},
timestamp = {Thu, 20 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/infsof/JefferySAKM15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fm/FernandezAKK15,
author = {Matthew Fernandez and
June Andronick and
Gerwin Klein and
Ihor Kuz},
editor = {Nikolaj S. Bj{\o}rner and
Frank S. de Boer},
title = {Automated Verification of {RPC} Stub Code},
booktitle = {{FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway,
June 24-26, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9109},
pages = {273--290},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-19249-9\_18},
doi = {10.1007/978-3-319-19249-9\_18},
timestamp = {Thu, 14 Apr 2022 20:26:16 +0200},
biburl = {https://dblp.org/rec/conf/fm/FernandezAKK15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icse/MatichukMAJKS15,
author = {Daniel Matichuk and
Toby C. Murray and
June Andronick and
D. Ross Jeffery and
Gerwin Klein and
Mark Staples},
editor = {Antonia Bertolino and
Gerardo Canfora and
Sebastian G. Elbaum},
title = {Empirical Study Towards a Leading Indicator for Cost of Formal Software
Verification},
booktitle = {37th {IEEE/ACM} International Conference on Software Engineering,
{ICSE} 2015, Florence, Italy, May 16-24, 2015, Volume 1},
pages = {722--732},
publisher = {{IEEE} Computer Society},
year = {2015},
url = {https://doi.org/10.1109/ICSE.2015.85},
doi = {10.1109/ICSE.2015.85},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/icse/MatichukMAJKS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/dagstuhl-reports/CoferKSW15,
author = {Darren D. Cofer and
Gerwin Klein and
Konrad Slind and
Virginie Wiels},
title = {Qualification of Formal Methods Tools (Dagstuhl Seminar 15182)},
journal = {Dagstuhl Reports},
volume = {5},
number = {4},
pages = {142--159},
year = {2015},
url = {https://doi.org/10.4230/DagRep.5.4.142},
doi = {10.4230/DAGREP.5.4.142},
timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/dagstuhl-reports/CoferKSW15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:books/sp/NipkowK14,
author = {Tobias Nipkow and
Gerwin Klein},
title = {Concrete Semantics - With Isabelle/HOL},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-10542-0},
doi = {10.1007/978-3-319-10542-0},
isbn = {978-3-319-10541-3},
timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/books/sp/NipkowK14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fac/DaumBK14,
author = {Matthias Daum and
Nelson Billing and
Gerwin Klein},
title = {Concerned with the unprivileged: user programs in kernel refinement},
journal = {Formal Aspects Comput.},
volume = {26},
number = {6},
pages = {1205--1229},
year = {2014},
url = {https://doi.org/10.1007/s00165-014-0296-9},
doi = {10.1007/S00165-014-0296-9},
timestamp = {Mon, 09 May 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/fac/DaumBK14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sigops/KellerMAOCRKH14,
author = {Gabriele Keller and
Toby C. Murray and
Sidney Amani and
Liam O'Connor and
Zilin Chen and
Leonid Ryzhyk and
Gerwin Klein and
Gernot Heiser},
title = {File systems deserve verification too!},
journal = {{ACM} {SIGOPS} Oper. Syst. Rev.},
volume = {48},
number = {1},
pages = {58--64},
year = {2014},
url = {https://doi.org/10.1145/2626401.2626414},
doi = {10.1145/2626401.2626414},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/sigops/KellerMAOCRKH14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tocs/KleinAEMSKH14,
author = {Gerwin Klein and
June Andronick and
Kevin Elphinstone and
Toby C. Murray and
Thomas Sewell and
Rafal Kolanski and
Gernot Heiser},
title = {Comprehensive formal verification of an {OS} microkernel},
journal = {{ACM} Trans. Comput. Syst.},
volume = {32},
number = {1},
pages = {2:1--2:70},
year = {2014},
url = {https://doi.org/10.1145/2560537},
doi = {10.1145/2560537},
timestamp = {Wed, 14 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tocs/KleinAEMSKH14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esem/StaplesJAMKK14,
author = {Mark Staples and
D. Ross Jeffery and
June Andronick and
Toby C. Murray and
Gerwin Klein and
Rafal Kolanski},
editor = {Maurizio Morisio and
Tore Dyb{\aa} and
Marco Torchiano},
title = {Productivity for proof engineering},
booktitle = {2014 {ACM-IEEE} International Symposium on Empirical Software Engineering
and Measurement, {ESEM} '14, Torino, Italy, September 18-19, 2014},
pages = {15:1--15:4},
publisher = {{ACM}},
year = {2014},
url = {https://doi.org/10.1145/2652524.2652551},
doi = {10.1145/2652524.2652551},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/esem/StaplesJAMKK14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fm/Klein14,
author = {Gerwin Klein},
editor = {Cliff B. Jones and
Pekka Pihlajasaari and
Jun Sun},
title = {Proof Engineering Considered Essential},
booktitle = {{FM} 2014: Formal Methods - 19th International Symposium, Singapore,
May 12-16, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8442},
pages = {16--21},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-06410-9\_2},
doi = {10.1007/978-3-319-06410-9\_2},
timestamp = {Tue, 14 May 2019 10:00:46 +0200},
biburl = {https://dblp.org/rec/conf/fm/Klein14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/GreenawayLAK14,
author = {David Greenaway and
Japheth Lim and
June Andronick and
Gerwin Klein},
editor = {Michael F. P. O'Boyle and
Keshav Pingali},
title = {Don't sweat the small stuff: formal verification of {C} code without
the pain},
booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
{PLDI} '14, Edinburgh, United Kingdom - June 09 - 11, 2014},
pages = {429--439},
publisher = {{ACM}},
year = {2014},
url = {https://doi.org/10.1145/2594291.2594296},
doi = {10.1145/2594291.2594296},
timestamp = {Thu, 24 Jun 2021 16:19:30 +0200},
biburl = {https://dblp.org/rec/conf/pldi/GreenawayLAK14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:series/natosec/KleinN14,
author = {Gerwin Klein and
Tobias Nipkow},
editor = {Orna Grumberg and
Helmut Seidl and
Maximilian Irlbeck},
title = {Applications of Interactive Proof to Data Flow Analysis and Security},
booktitle = {Software Systems Safety},
series = {{NATO} Science for Peace and Security Series, {D:} Information and
Communication Security},
volume = {36},
pages = {77--134},
publisher = {{IOS} Press},
year = {2014},
url = {https://doi.org/10.3233/978-1-61499-385-8-77},
doi = {10.3233/978-1-61499-385-8-77},
timestamp = {Tue, 16 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/series/natosec/KleinN14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/itp/2014,
editor = {Gerwin Klein and
Ruben Gamboa},
title = {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},
series = {Lecture Notes in Computer Science},
volume = {8558},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08970-6},
doi = {10.1007/978-3-319-08970-6},
isbn = {978-3-319-08969-0},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/2014.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfem/BoytonABFGGKLS13,
author = {Andrew Boyton and
June Andronick and
Callum Bannister and
Matthew Fernandez and
Xin Gao and
David Greenaway and
Gerwin Klein and
Corey Lewis and
Thomas Sewell},
editor = {Lindsay Groves and
Jing Sun},
title = {Formally Verified System Initialisation},
booktitle = {Formal Methods and Software Engineering - 15th International Conference
on Formal Engineering Methods, {ICFEM} 2013, Queenstown, New Zealand,
October 29 - November 1, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8144},
pages = {70--85},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-41202-8\_6},
doi = {10.1007/978-3-642-41202-8\_6},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/icfem/BoytonABFGGKLS13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icse/StaplesKKLAMJB04,
author = {Mark Staples and
Rafal Kolanski and
Gerwin Klein and
Corey Lewis and
June Andronick and
Toby C. Murray and
D. Ross Jeffery and
Len Bass},
editor = {David Notkin and
Betty H. C. Cheng and
Klaus Pohl},
title = {Formal specifications better than function points for code sizing},
booktitle = {35th International Conference on Software Engineering, {ICSE} '13,
San Francisco, CA, USA, May 18-26, 2013},
pages = {1257--1260},
publisher = {{IEEE} Computer Society},
year = {2013},
url = {https://doi.org/10.1109/ICSE.2013.6606692},
doi = {10.1109/ICSE.2013.6606692},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/icse/StaplesKKLAMJB04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/SewellMK13,
author = {Thomas Arthur Leck Sewell and
Magnus O. Myreen and
Gerwin Klein},
editor = {Hans{-}Juergen Boehm and
Cormac Flanagan},
title = {Translation validation for a verified {OS} kernel},
booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
{PLDI} '13, Seattle, WA, USA, June 16-19, 2013},
pages = {471--482},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2491956.2462183},
doi = {10.1145/2491956.2462183},
timestamp = {Fri, 30 Nov 2018 12:21:40 +0100},
biburl = {https://dblp.org/rec/conf/pldi/SewellMK13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sosp/KellerMAOCRKH13,
author = {Gabriele Keller and
Toby C. Murray and
Sidney Amani and
Liam O'Connor and
Zilin Chen and
Leonid Ryzhyk and
Gerwin Klein and
Gernot Heiser},
editor = {Tim Harris and
Anil Madhavapeddy},
title = {File systems deserve verification too!},
booktitle = {Proceedings of the Seventh Workshop on Programming Languages and Operating
Systems, {PLOS} 2013, Farmington, Pennsylvania, USA, November 3-6,
2013},
pages = {1:1--1:7},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2525528.2525530},
doi = {10.1145/2525528.2525530},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/sosp/KellerMAOCRKH13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sosp/FernandezKKA13,
author = {Matthew Fernandez and
Ihor Kuz and
Gerwin Klein and
June Andronick},
editor = {Tim Harris and
Anil Madhavapeddy},
title = {Towards a verified component platform},
booktitle = {Proceedings of the Seventh Workshop on Programming Languages and Operating
Systems, {PLOS} 2013, Farmington, Pennsylvania, USA, November 3-6,
2013},
pages = {2:1--2:7},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2525528.2525535},
doi = {10.1145/2525528.2525535},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/sosp/FernandezKKA13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sp/MurrayMBGBSLGK13,
author = {Toby C. Murray and
Daniel Matichuk and
Matthew Brassil and
Peter Gammie and
Timothy Bourke and
Sean Seefried and
Corey Lewis and
Xin Gao and
Gerwin Klein},
title = {seL4: From General Purpose to a Proof of Information Flow Enforcement},
booktitle = {2013 {IEEE} Symposium on Security and Privacy, {SP} 2013, Berkeley,
CA, USA, May 19-22, 2013},
pages = {415--429},
publisher = {{IEEE} Computer Society},
year = {2013},
url = {https://doi.org/10.1109/SP.2013.35},
doi = {10.1109/SP.2013.35},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/sp/MurrayMBGBSLGK13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/KleinKB12,
author = {Gerwin Klein and
Rafal Kolanski and
Andrew Boyton},
title = {Separation Algebra},
journal = {Arch. Formal Proofs},
volume = {2012},
year = {2012},
url = {https://www.isa-afp.org/entries/Separation\_Algebra.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/KleinKB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/aim/BarnesBCDKSSSTHW12,
author = {Nick Barnes and
Peter Baumgartner and
Tib{\'{e}}rio S. Caetano and
Hugh F. Durrant{-}Whyte and
Gerwin Klein and
Penelope Sanderson and
Abdul Sattar and
Peter J. Stuckey and
Sylvie Thi{\'{e}}baux and
Pascal Van Hentenryck and
Toby Walsh},
title = {AI@NICTA},
journal = {{AI} Mag.},
volume = {33},
number = {3},
pages = {115},
year = {2012},
url = {https://doi.org/10.1609/aimag.v33i3.2430},
doi = {10.1609/AIMAG.V33I3.2430},
timestamp = {Tue, 25 Aug 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/aim/BarnesBCDKSSSTHW12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ieeesp/HeiserMK12,
author = {Gernot Heiser and
Toby C. Murray and
Gerwin Klein},
title = {It's Time for Trustworthy Systems},
journal = {{IEEE} Secur. Priv.},
volume = {10},
number = {2},
pages = {67--70},
year = {2012},
url = {https://doi.org/10.1109/MSP.2012.41},
doi = {10.1109/MSP.2012.41},
timestamp = {Sun, 15 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/ieeesp/HeiserMK12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/aisc/BourkeDKK12,
author = {Timothy Bourke and
Matthias Daum and
Gerwin Klein and
Rafal Kolanski},
editor = {Johan Jeuring and
John A. Campbell and
Jacques Carette and
Gabriel Dos Reis and
Petr Sojka and
Makarius Wenzel and
Volker Sorge},
title = {Challenges and Experiences in Managing Large-Scale Proofs},
booktitle = {Intelligent Computer Mathematics - 11th International Conference,
{AISC} 2012, 19th Symposium, Calculemus 2012, 5th International Workshop,
{DML} 2012, 11th International Conference, {MKM} 2012, Systems and
Projects, Held as Part of {CICM} 2012, Bremen, Germany, July 8-13,
2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7362},
pages = {32--48},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-31374-5\_3},
doi = {10.1007/978-3-642-31374-5\_3},
timestamp = {Sun, 02 Jun 2019 21:23:46 +0200},
biburl = {https://dblp.org/rec/conf/aisc/BourkeDKK12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MurrayMBGK12,
author = {Toby C. Murray and
Daniel Matichuk and
Matthew Brassil and
Peter Gammie and
Gerwin Klein},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Noninterference for Operating System Kernels},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {126--142},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_12},
doi = {10.1007/978-3-642-35308-6\_12},
timestamp = {Wed, 07 Dec 2022 23:14:04 +0100},
biburl = {https://dblp.org/rec/conf/cpp/MurrayMBGK12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icse/AndronickJKKSZZ12,
author = {June Andronick and
D. Ross Jeffery and
Gerwin Klein and
Rafal Kolanski and
Mark Staples and
He Zhang and
Liming Zhu},
editor = {Martin Glinz and
Gail C. Murphy and
Mauro Pezz{\`{e}}},
title = {Large-scale formal verification in practice: {A} process perspective},
booktitle = {34th International Conference on Software Engineering, {ICSE} 2012,
June 2-9, 2012, Zurich, Switzerland},
pages = {1002--1011},
publisher = {{IEEE} Computer Society},
year = {2012},
url = {https://doi.org/10.1109/ICSE.2012.6227120},
doi = {10.1109/ICSE.2012.6227120},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/icse/AndronickJKKSZZ12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ispw/ZhangKSAZK12,
author = {He Zhang and
Gerwin Klein and
Mark Staples and
June Andronick and
Liming Zhu and
Rafal Kolanski},
editor = {D. Ross Jeffery and
David Raffo and
Ove Armbrust and
LiGuo Huang},
title = {Simulation modeling of a large-scale formal verification process},
booktitle = {2012 International Conference on Software and System Process, {ICSSP}
2012, Zurich, Switzerland, June 2-3, 2012},
pages = {3--12},
publisher = {{IEEE} Computer Society},
year = {2012},
url = {https://doi.org/10.1109/ICSSP.2012.6225979},
doi = {10.1109/ICSSP.2012.6225979},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ispw/ZhangKSAZK12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/GreenawayAK12,
author = {David Greenaway and
June Andronick and
Gerwin Klein},
editor = {Lennart Beringer and
Amy P. Felty},
title = {Bridging the Gap: Automatic Verified Abstraction of {C}},
booktitle = {Interactive Theorem Proving - Third International Conference, {ITP}
2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7406},
pages = {99--115},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-32347-8\_8},
doi = {10.1007/978-3-642-32347-8\_8},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/GreenawayAK12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/KleinKB12,
author = {Gerwin Klein and
Rafal Kolanski and
Andrew Boyton},
editor = {Lennart Beringer and
Amy P. Felty},
title = {Mechanised Separation Algebra},
booktitle = {Interactive Theorem Proving - Third International Conference, {ITP}
2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7406},
pages = {332--337},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-32347-8\_22},
doi = {10.1007/978-3-642-32347-8\_22},
timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/itp/KleinKB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:series/natosec/Klein12,
author = {Gerwin Klein},
editor = {Tobias Nipkow and
Orna Grumberg and
Benedikt Hauptmann},
title = {Interactive Proof: Applications to Semantics},
booktitle = {Software Safety and Security - Tools for Analysis and Verification},
series = {{NATO} Science for Peace and Security Series - {D:} Information and
Communication Security},
volume = {33},
pages = {85--125},
publisher = {{IOS} Press},
year = {2012},
url = {https://doi.org/10.3233/978-1-61499-028-4-85},
doi = {10.3233/978-1-61499-028-4-85},
timestamp = {Wed, 04 Mar 2020 14:10:38 +0100},
biburl = {https://dblp.org/rec/series/natosec/Klein12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-1211-5873,
editor = {Franck Cassez and
Ralf Huuck and
Gerwin Klein and
Bastian Schlich},
title = {Proceedings Seventh Conference on Systems Software Verification, {SSV}
2012, Sydney, Australia, 28-30 November 2012},
series = {{EPTCS}},
volume = {102},
year = {2012},
url = {https://doi.org/10.4204/EPTCS.102},
doi = {10.4204/EPTCS.102},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1211-5873.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/hotos/KleinMGSW11,
author = {Gerwin Klein and
Toby C. Murray and
Peter Gammie and
Thomas Sewell and
Simon Winwood},
editor = {Matt Welsh},
title = {Provable Security: How Feasible Is It?},
booktitle = {13th Workshop on Hot Topics in Operating Systems, HotOS XIII, Napa,
California, USA, May 9-11, 2011},
publisher = {{USENIX} Association},
year = {2011},
url = {https://www.usenix.org/conference/hotosxiii/provable-security-how-feasible-it},
timestamp = {Wed, 04 Jul 2018 13:06:34 +0200},
biburl = {https://dblp.org/rec/conf/hotos/KleinMGSW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/SewellWGMAK11,
author = {Thomas Sewell and
Simon Winwood and
Peter Gammie and
Toby C. Murray and
June Andronick and
Gerwin Klein},
editor = {Marko C. J. D. van Eekelen and
Herman Geuvers and
Julien Schmaltz and
Freek Wiedijk},
title = {seL4 Enforces Integrity},
booktitle = {Interactive Theorem Proving - Second International Conference, {ITP}
2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6898},
pages = {325--340},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-22863-6\_24},
doi = {10.1007/978-3-642-22863-6\_24},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/SewellWGMAK11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cacm/KleinAEHCDEEKNSTW10,
author = {Gerwin Klein and
June Andronick and
Kevin Elphinstone and
Gernot Heiser and
David A. Cock and
Philip Derrin and
Dhammika Elkaduwe and
Kai Engelhardt and
Rafal Kolanski and
Michael Norrish and
Thomas Sewell and
Harvey Tuch and
Simon Winwood},
title = {seL4: formal verification of an operating-system kernel},
journal = {Commun. {ACM}},
volume = {53},
number = {6},
pages = {107--115},
year = {2010},
url = {https://doi.org/10.1145/1743546.1743574},
doi = {10.1145/1743546.1743574},
timestamp = {Wed, 21 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/cacm/KleinAEHCDEEKNSTW10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/aplas/Klein10,
author = {Gerwin Klein},
editor = {Kazunori Ueda},
title = {From a Verified Kernel towards Verified Systems},
booktitle = {Programming Languages and Systems - 8th Asian Symposium, {APLAS} 2010,
Shanghai, China, November 28 - December 1, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6461},
pages = {21--33},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-17164-2\_3},
doi = {10.1007/978-3-642-17164-2\_3},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/aplas/Klein10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/HeiserAEKKR10,
author = {Gernot Heiser and
June Andronick and
Kevin Elphinstone and
Gerwin Klein and
Ihor Kuz and
Leonid Ryzhyk},
editor = {Shouhuai Xu and
N. Asokan and
Ahmad{-}Reza Sadeghi},
title = {The road to trustworthy systems},
booktitle = {Proceedings of the fifth {ACM} workshop on Scalable trusted computing,
STC@CCS 2010, Chicago, IL, USA, October 4, 2010},
pages = {3--10},
publisher = {{ACM}},
year = {2010},
url = {http://dl.acm.org/citation.cfm?id=1867638},
timestamp = {Tue, 10 Nov 2020 16:06:16 +0100},
biburl = {https://dblp.org/rec/conf/ccs/HeiserAEKKR10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/Klein10,
author = {Gerwin Klein},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
title = {A Formally Verified {OS} Kernel. Now What?},
booktitle = {Interactive Theorem Proving, First International Conference, {ITP}
2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {1--7},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_1},
doi = {10.1007/978-3-642-14052-5\_1},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/Klein10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sigcomm/KuzKLW10,
author = {Ihor Kuz and
Gerwin Klein and
Corey Lewis and
Adam Walker},
editor = {Chandramohan A. Thekkath and
Ramakrishna Kotla and
Lidong Zhou},
title = {capDL: a language for describing capability-based systems},
booktitle = {Proceedings of the 1st {ACM} {SIGCOMM} Asia-Pacific Workshop on Systems,
ApSys 2010, New Delhi, India, August 30, 2010},
pages = {31--36},
publisher = {{ACM}},
year = {2010},
url = {https://doi.org/10.1145/1851276.1851284},
doi = {10.1145/1851276.1851284},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/sigcomm/KuzKLW10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vstte/Klein10,
author = {Gerwin Klein},
editor = {Gary T. Leavens and
Peter W. O'Hearn and
Sriram K. Rajamani},
title = {The L4.verified Project - Next Steps},
booktitle = {Verified Software: Theories, Tools, Experiments, Third International
Conference, {VSTTE} 2010, Edinburgh, UK, August 16-19, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6217},
pages = {86--96},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-15057-9\_6},
doi = {10.1007/978-3-642-15057-9\_6},
timestamp = {Tue, 14 May 2019 10:00:49 +0200},
biburl = {https://dblp.org/rec/conf/vstte/Klein10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/sp/10/KleinSW10,
author = {Gerwin Klein and
Thomas Sewell and
Simon Winwood},
editor = {David S. Hardin},
title = {Refinement in the Formal Verification of the seL4 Microkernel},
booktitle = {Design and Verification of Microprocessor Systems for High-Assurance
Applications},
pages = {323--339},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-1-4419-1539-9\_11},
doi = {10.1007/978-1-4419-1539-9\_11},
timestamp = {Wed, 29 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/sp/10/KleinSW10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ssv/2010,
editor = {Ralf Huuck and
Gerwin Klein and
Bastian Schlich},
title = {5th International Workshop on Systems Software Verification, SSV'10,
Vancouver, BC, Canada, October 6-7, 2010},
publisher = {{USENIX} Association},
year = {2010},
url = {https://www.usenix.org/conference/ssv10},
timestamp = {Wed, 04 Jul 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ssv/2010.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/KleinHS09,
author = {Gerwin Klein and
Ralf Huuck and
Bastian Schlich},
title = {Operating System Verification},
journal = {J. Autom. Reason.},
volume = {42},
number = {2-4},
pages = {123--124},
year = {2009},
url = {https://doi.org/10.1007/s10817-009-9126-9},
doi = {10.1007/S10817-009-9126-9},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/KleinHS09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/usenix-login/Klein09,
author = {Gerwin Klein},
title = {Correct {OS} Kernel? Proof? Done!},
journal = {login Usenix Mag.},
volume = {34},
number = {6},
year = {2009},
url = {https://www.usenix.org/publications/login/december-2009-volume-34-number-6/correct-os-kernel-proof-done},
timestamp = {Thu, 02 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/usenix-login/Klein09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/KleinDE09,
author = {Gerwin Klein and
Philip Derrin and
Kevin Elphinstone},
editor = {Graham Hutton and
Andrew P. Tolmach},
title = {Experience report: seL4: formally verifying a high-performance microkernel},
booktitle = {Proceeding of the 14th {ACM} {SIGPLAN} international conference on
Functional programming, {ICFP} 2009, Edinburgh, Scotland, UK, August
31 - September 2, 2009},
pages = {91--96},
publisher = {{ACM}},
year = {2009},
url = {https://doi.org/10.1145/1596550.1596566},
doi = {10.1145/1596550.1596566},
timestamp = {Fri, 25 Jun 2021 14:48:54 +0200},
biburl = {https://dblp.org/rec/conf/icfp/KleinDE09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sosp/KleinEHACDEEKNSTW09,
author = {Gerwin Klein and
Kevin Elphinstone and
Gernot Heiser and
June Andronick and
David A. Cock and
Philip Derrin and
Dhammika Elkaduwe and
Kai Engelhardt and
Rafal Kolanski and
Michael Norrish and
Thomas Sewell and
Harvey Tuch and
Simon Winwood},
editor = {Jeanna Neefe Matthews and
Thomas E. Anderson},
title = {se{L}4: formal verification of an OS kernel.},
booktitle = {Proceedings of the 22nd {ACM} Symposium on Operating Systems Principles
2009, {SOSP} 2009, Big Sky, Montana, USA, October 11-14, 2009},
pages = {207--220},
publisher = {{ACM}},
year = {2009},
url = {https://doi.org/10.1145/1629575.1629596},
doi = {10.1145/1629575.1629596},
timestamp = {Sun, 04 Aug 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/sosp/KleinEHACDEEKNSTW09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/KolanskiK09,
author = {Rafal Kolanski and
Gerwin Klein},
editor = {Stefan Berghofer and
Tobias Nipkow and
Christian Urban and
Makarius Wenzel},
title = {Types, Maps and Separation Logic},
booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference,
TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5674},
pages = {276--292},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-03359-9\_20},
doi = {10.1007/978-3-642-03359-9\_20},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/KolanskiK09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/WinwoodKSACN09,
author = {Simon Winwood and
Gerwin Klein and
Thomas Sewell and
June Andronick and
David A. Cock and
Michael Norrish},
editor = {Stefan Berghofer and
Tobias Nipkow and
Christian Urban and
Makarius Wenzel},
title = {Mind the Gap},
booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference,
TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5674},
pages = {500--515},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-03359-9\_34},
doi = {10.1007/978-3-642-03359-9\_34},
timestamp = {Wed, 21 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/tphol/WinwoodKSACN09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/HuuckKS09,
author = {Ralf Huuck and
Gerwin Klein and
Bastian Schlich},
editor = {Ralf Huuck and
Gerwin Klein and
Bastian Schlich},
title = {Preface},
booktitle = {Proceedings of the 4th International Workshop on Systems Software
Verification, {SSV} 2009, Aachen, Germany, June 22-24, 2009},
series = {Electronic Notes in Theoretical Computer Science},
volume = {254},
pages = {1--3},
publisher = {Elsevier},
year = {2009},
url = {https://doi.org/10.1016/j.entcs.2009.09.056},
doi = {10.1016/J.ENTCS.2009.09.056},
timestamp = {Fri, 17 Feb 2023 10:35:59 +0100},
biburl = {https://dblp.org/rec/journals/entcs/HuuckKS09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BeckertK08,
author = {Bernhard Beckert and
Gerwin Klein},
editor = {Bernhard Beckert and
Gerwin Klein},
title = {Title, Preface, Table of Contents},
booktitle = {Proceedings of the 5th International Verification Workshop in connection
with {IJCAR} 2008, Sydney, Australia, August 10-11, 2008},
series = {{CEUR} Workshop Proceedings},
volume = {372},
publisher = {CEUR-WS.org},
year = {2008},
url = {https://ceur-ws.org/Vol-372/front.pdf},
timestamp = {Fri, 10 Mar 2023 16:23:14 +0100},
biburl = {https://dblp.org/rec/conf/cade/BeckertK08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/CockKS08,
author = {David A. Cock and
Gerwin Klein and
Thomas Sewell},
editor = {Otmane A{\"{\i}}t Mohamed and
C{\'{e}}sar A. Mu{\~{n}}oz and
Sofi{\`{e}}ne Tahar},
title = {Secure Microkernels, State Monads and Scalable Refinement},
booktitle = {Theorem Proving in Higher Order Logics, 21st International Conference,
TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5170},
pages = {167--182},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-71067-7\_16},
doi = {10.1007/978-3-540-71067-7\_16},
timestamp = {Wed, 21 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/tphol/CockKS08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vstte/KolanskiK08,
author = {Rafal Kolanski and
Gerwin Klein},
editor = {Natarajan Shankar and
Jim Woodcock},
title = {Mapped Separation Logic},
booktitle = {Verified Software: Theories, Tools, Experiments, Second International
Conference, {VSTTE} 2008, Toronto, Canada, October 6-9, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5295},
pages = {15--29},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87873-5\_6},
doi = {10.1007/978-3-540-87873-5\_6},
timestamp = {Fri, 17 Feb 2023 09:02:02 +0100},
biburl = {https://dblp.org/rec/conf/vstte/KolanskiK08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vstte/ElkaduweKE08,
author = {Dhammika Elkaduwe and
Gerwin Klein and
Kevin Elphinstone},
editor = {Natarajan Shankar and
Jim Woodcock},
title = {Verified Protection Model of the seL4 Microkernel},
booktitle = {Verified Software: Theories, Tools, Experiments, Second International
Conference, {VSTTE} 2008, Toronto, Canada, October 6-9, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5295},
pages = {99--114},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87873-5\_11},
doi = {10.1007/978-3-540-87873-5\_11},
timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/vstte/ElkaduweKE08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/HuuckKS08,
author = {Ralf Huuck and
Gerwin Klein and
Bastian Schlich},
editor = {Ralf Huuck and
Gerwin Klein and
Bastian Schlich},
title = {Preface},
booktitle = {Proceedings of the 3rd International Workshop on Systems Software
Verification, {SSV} 2008, Sydney, Australia, February 25-27, 2008},
series = {Electronic Notes in Theoretical Computer Science},
volume = {217},
pages = {1--3},
publisher = {Elsevier},
year = {2008},
url = {https://doi.org/10.1016/j.entcs.2008.06.038},
doi = {10.1016/J.ENTCS.2008.06.038},
timestamp = {Fri, 17 Feb 2023 10:34:05 +0100},
biburl = {https://dblp.org/rec/journals/entcs/HuuckKS08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2008verify,
editor = {Bernhard Beckert and
Gerwin Klein},
title = {Proceedings of the 5th International Verification Workshop in connection
with {IJCAR} 2008, Sydney, Australia, August 10-11, 2008},
series = {{CEUR} Workshop Proceedings},
volume = {372},
publisher = {CEUR-WS.org},
year = {2008},
url = {https://ceur-ws.org/Vol-372},
urn = {urn:nbn:de:0074-372-1},
timestamp = {Fri, 10 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cade/2008verify.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ssv/2008,
editor = {Ralf Huuck and
Gerwin Klein and
Bastian Schlich},
title = {Proceedings of the 3rd International Workshop on Systems Software
Verification, {SSV} 2008, Sydney, Australia, February 25-27, 2008},
series = {Electronic Notes in Theoretical Computer Science},
volume = {217},
publisher = {Elsevier},
year = {2008},
url = {https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/217/suppl/C},
timestamp = {Fri, 17 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ssv/2008.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ssv/2009,
editor = {Ralf Huuck and
Gerwin Klein and
Bastian Schlich},
title = {Proceedings of the 4th International Workshop on Systems Software
Verification, {SSV} 2009, Aachen, Germany, June 22-24, 2009},
series = {Electronic Notes in Theoretical Computer Science},
volume = {254},
publisher = {Elsevier},
year = {2008},
url = {https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/254/suppl/C},
timestamp = {Fri, 17 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ssv/2009.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sigops/HeiserEKKP07,
author = {Gernot Heiser and
Kevin Elphinstone and
Ihor Kuz and
Gerwin Klein and
Stefan M. Petters},
title = {Towards trustworthy computing systems: taking microkernels to the
next level},
journal = {{ACM} {SIGOPS} Oper. Syst. Rev.},
volume = {41},
number = {4},
pages = {3--11},
year = {2007},
url = {https://doi.org/10.1145/1278901.1278904},
doi = {10.1145/1278901.1278904},
timestamp = {Tue, 14 Jul 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sigops/HeiserEKKP07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/MengPK07,
author = {Jia Meng and
Lawrence C. Paulson and
Gerwin Klein},
editor = {Bernhard Beckert},
title = {A Termination Checker for Isabelle Hoare Logic},
booktitle = {Proceedings of 4th International Verification Workshop in connection
with CADE-21, Bremen, Germany, July 15-16, 2007},
series = {{CEUR} Workshop Proceedings},
volume = {259},
publisher = {CEUR-WS.org},
year = {2007},
url = {https://ceur-ws.org/Vol-259/paper10.pdf},
timestamp = {Tue, 28 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/MengPK07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/hotos/ElphinstoneKDRH07,
author = {Kevin Elphinstone and
Gerwin Klein and
Philip Derrin and
Timothy Roscoe and
Gernot Heiser},
editor = {Galen C. Hunt},
title = {Towards a Practical, Verified Kernel},
booktitle = {Proceedings of HotOS'07: 11th Workshop on Hot Topics in Operating
Systems, May 7-9, 2005, San Diego, California, {USA}},
publisher = {{USENIX} Association},
year = {2007},
url = {http://www.usenix.org/events/hotos07/tech/full\_papers/elphinstone/elphinstone.pdf},
timestamp = {Thu, 12 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/hotos/ElphinstoneKDRH07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/TuchKN07,
author = {Harvey Tuch and
Gerwin Klein and
Michael Norrish},
editor = {Martin Hofmann and
Matthias Felleisen},
title = {Types, bytes, and separation logic},
booktitle = {Proceedings of the 34th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
of Programming Languages, {POPL} 2007, Nice, France, January 17-19,
2007},
pages = {97--108},
publisher = {{ACM}},
year = {2007},
url = {https://doi.org/10.1145/1190216.1190234},
doi = {10.1145/1190216.1190234},
timestamp = {Sun, 04 Aug 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/popl/TuchKN07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/toplas/KleinN06,
author = {Gerwin Klein and
Tobias Nipkow},
title = {A machine-checked model for a Java-like language, virtual machine,
and compiler},
journal = {{ACM} Trans. Program. Lang. Syst.},
volume = {28},
number = {4},
pages = {619--695},
year = {2006},
url = {https://doi.org/10.1145/1146809.1146811},
doi = {10.1145/1146809.1146811},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/toplas/KleinN06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cats/KolanskiK06,
author = {Rafal Kolanski and
Gerwin Klein},
editor = {Joachim Gudmundsson and
C. Barry Jay},
title = {Formalising the {L4} microkernel {API}},
booktitle = {Theory of Computing 2006, Proceedings of the Twelfth Computing: The
Australasian Theory Symposium {(CATS2006).} Hobart, Tasmania, Australia,
16-19 January 2006, Proceedings},
series = {{CRPIT}},
volume = {51},
pages = {53--68},
publisher = {Australian Computer Society},
year = {2006},
url = {http://crpit.scem.westernsydney.edu.au/abstracts/CRPITV51Kolanski.html},
timestamp = {Mon, 08 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cats/KolanskiK06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/haskell/DerrinEKCC06,
author = {Philip Derrin and
Kevin Elphinstone and
Gerwin Klein and
David A. Cock and
Manuel M. T. Chakravarty},
editor = {Andres L{\"{o}}h},
title = {Running the manual: an approach to high-assurance microkernel development},
booktitle = {Proceedings of the {ACM} {SIGPLAN} Workshop on Haskell, Haskell 2006,
Portland, Oregon, USA, September 17, 2006},
pages = {60--71},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1159842.1159850},
doi = {10.1145/1159842.1159850},
timestamp = {Wed, 21 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/haskell/DerrinEKCC06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lopstr/WinwoodKC06,
author = {Simon Winwood and
Gerwin Klein and
Manuel M. T. Chakravarty},
editor = {Germ{\'{a}}n Puebla},
title = {On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors},
booktitle = {Logic-Based Program Synthesis and Transformation, 16th International
Symposium, {LOPSTR} 2006, Venice, Italy, July 12-14, 2006, Revised
Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {4407},
pages = {111--126},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/978-3-540-71410-1\_9},
doi = {10.1007/978-3-540-71410-1\_9},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/lopstr/WinwoodKC06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/KleinN05,
author = {Gerwin Klein and
Tobias Nipkow},
title = {Jinja is not Java},
journal = {Arch. Formal Proofs},
volume = {2005},
year = {2005},
url = {https://www.isa-afp.org/entries/Jinja.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/KleinN05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/it/Klein05,
author = {Gerwin Klein},
title = {Verified Java Bytecode Verification (Verified Java Bytecode Verification)},
journal = {it Inf. Technol.},
volume = {47},
number = {2},
pages = {107--110},
year = {2005},
url = {https://doi.org/10.1524/itit.47.2.107.62257},
doi = {10.1524/ITIT.47.2.107.62257},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/it/Klein05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/hotos/TuchKH05,
author = {Harvey Tuch and
Gerwin Klein and
Gernot Heiser},
title = {{OS} Verification - Now!},
booktitle = {Proceedings of HotOS'05: 10th Workshop on Hot Topics in Operating
Systems, June 12-15, 2005, Santa Fe, New Mexico, {USA}},
publisher = {{USENIX} Association},
year = {2005},
url = {http://www.usenix.org/events/hotos05/final\_papers/full\_papers/tuch/tuch.pdf},
timestamp = {Thu, 12 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/hotos/TuchKH05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/TuchK05,
author = {Harvey Tuch and
Gerwin Klein},
editor = {Geoff Sutcliffe and
Andrei Voronkov},
title = {A Unified Memory Model for Pointers},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 12th
International Conference, {LPAR} 2005, Montego Bay, Jamaica, December
2-6, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3835},
pages = {474--488},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11591191\_33},
doi = {10.1007/11591191\_33},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/lpar/TuchK05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/Klein04,
author = {Gerwin Klein},
title = {Example Submission},
journal = {Arch. Formal Proofs},
volume = {2004},
year = {2004},
url = {https://www.isa-afp.org/entries/Example-Submission.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/Klein04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jlp/KleinS04,
author = {Gerwin Klein and
Martin Strecker},
title = {Verified bytecode verification and type-certifying compilation},
journal = {J. Log. Algebraic Methods Program.},
volume = {58},
number = {1-2},
pages = {27--60},
year = {2004},
url = {https://doi.org/10.1016/j.jlap.2003.07.004},
doi = {10.1016/J.JLAP.2003.07.004},
timestamp = {Tue, 16 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jlp/KleinS04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ifipTCS/WildmoserNKN04,
author = {Martin Wildmoser and
Tobias Nipkow and
Gerwin Klein and
Sebastian Nanz},
editor = {Jean{-}Jacques L{\'{e}}vy and
Ernst W. Mayr and
John C. Mitchell},
title = {Prototyping Proof Carrying Code},
booktitle = {Exploring New Frontiers of Theoretical Informatics, {IFIP} 18th World
Computer Congress, {TC1} 3rd International Conference on Theoretical
Computer Science (TCS2004), 22-27 August 2004, Toulouse, France},
series = {{IFIP}},
volume = {155},
pages = {333--347},
publisher = {Kluwer/Springer},
year = {2004},
url = {https://doi.org/10.1007/1-4020-8141-3\_27},
doi = {10.1007/1-4020-8141-3\_27},
timestamp = {Fri, 27 Sep 2019 10:35:17 +0200},
biburl = {https://dblp.org/rec/conf/ifipTCS/WildmoserNKN04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{DBLP:phd/dnb/Klein03a,
author = {Gerwin Klein},
title = {Verified Java bytecode verification},
school = {Technical University Munich, Germany},
year = {2003},
url = {http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2003/klein.html},
urn = {urn:nbn:de:bvb:91-diss2003021717180},
timestamp = {Sat, 17 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/phd/dnb/Klein03a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/KleinW03,
author = {Gerwin Klein and
Martin Wildmoser},
title = {Verified Bytecode Subroutines},
journal = {J. Autom. Reason.},
volume = {30},
number = {3-4},
pages = {363--398},
year = {2003},
url = {https://doi.org/10.1023/A:1025095122199},
doi = {10.1023/A:1025095122199},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/KleinW03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/KleinN03,
author = {Gerwin Klein and
Tobias Nipkow},
title = {Verified bytecode verifiers},
journal = {Theor. Comput. Sci.},
volume = {298},
number = {3},
pages = {583--626},
year = {2003},
url = {https://doi.org/10.1016/S0304-3975(02)00869-1},
doi = {10.1016/S0304-3975(02)00869-1},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tcs/KleinN03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/KleinW03,
author = {Gerwin Klein and
Martin Wildmoser},
editor = {David A. Basin and
Burkhart Wolff},
title = {Verified Bytecode Subroutines},
booktitle = {Theorem Proving in Higher Order Logics, 16th International Conference,
TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2758},
pages = {55--70},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/10930755\_4},
doi = {10.1007/10930755\_4},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/KleinW03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:conf/gi/Klein03,
author = {Gerwin Klein},
editor = {Heinz Beilner and
Thomas Dreier and
Markus Gross and
Oliver G{\"{u}}nther and
Steffen H{\"{o}}lldobler and
Klaus{-}Peter L{\"{o}}hr and
R{\"{u}}diger Reischuk and
Dorothea Wagner},
title = {Verified Java Bytecode Verification},
booktitle = {Ausgezeichnete Informatikdissertationen 2003},
series = {{LNI}},
volume = {{D-4}},
pages = {91--100},
publisher = {{GI}},
year = {2003},
url = {https://dl.gi.de/handle/20.500.12116/4471},
timestamp = {Tue, 04 Jul 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/gi/Klein03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/concurrency/KleinN01,
author = {Gerwin Klein and
Tobias Nipkow},
title = {Verified lightweight bytecode verification},
journal = {Concurr. Comput. Pract. Exp.},
volume = {13},
number = {13},
pages = {1133--1151},
year = {2001},
url = {https://doi.org/10.1002/cpe.597},
doi = {10.1002/CPE.597},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/concurrency/KleinN01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/hci/BrandlK99,
author = {Alfons Brandl and
Gerwin Klein},
editor = {Hans{-}J{\"{o}}rg Bullinger and
J{\"{u}}rgen Ziegler},
title = {FormGen: {A} Generator for Adaptive Forms Based on EasyGUI},
booktitle = {Human-Computer Interaction: Ergonomics and User Interfaces, Proceedings
of {HCI} International '99 (the 8th International Conference on Human-Computer
Interaction), Munich, Germany, August 22-26, 1999, Volume 1},
pages = {1172--1176},
publisher = {Lawrence Erlbaum},
year = {1999},
timestamp = {Wed, 07 Jan 2015 19:13:32 +0100},
biburl = {https://dblp.org/rec/conf/hci/BrandlK99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-08-05 21:17 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
