Publications

2023

[1] James Patrick-Evans, Moritz Dannehl, and Johannes Kinder. XFL: Naming Functions in Binaries with Extreme Multi-label Learning. In Proc. IEEE Symp. Security and Privacy (S&P), IEEE, 2023. to appear. BibTeX PDF
@inproceedings{oakland23-xfl,
    author = {James Patrick-Evans and Moritz Dannehl and Johannes Kinder},
    booktitle = {Proc. IEEE Symp. Security and Privacy (S\&P)},
    note = {to appear},
    publisher = {IEEE},
    title = {XFL: Naming Functions in Binaries with Extreme Multi-label Learning},
    year = {2023}
}

2022

[2] Hernán Ponce de León and Johannes Kinder. Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks. In Proc. IEEE Symp. Security and Privacy (S&P), pp. 1415–1428, IEEE, 2022. BibTeX PDF
@inproceedings{oakland22-cats-vs-spectre,
    author = {Hern{\'a}n Ponce de Le{\'o}n and Johannes Kinder},
    booktitle = {Proc. IEEE Symp. Security and Privacy (S\&P)},
    doi = {10.1109/SP46214.2022.00082},
    pages = {1415--1428},
    publisher = {IEEE},
    title = {Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks},
    year = {2022}
}

[3] Hernán Ponce de León, Thomas Haas, and Roland Meyer. Dartagnan: SMT-based Violation Witness Validation (Competition Contribution). In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 418–423, Springer, 2022. BibTeX
@inproceedings{tacas22-dartagnan,
    author = {Hern{\'a}n Ponce de Le{\'o}n and Thomas Haas and Roland Meyer},
    booktitle = {Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
    doi = {10.1007/978-3-030-99527-0\_24},
    pages = {418--423},
    publisher = {Springer},
    series = {LNCS},
    title = {Dartagnan: SMT-based Violation Witness Validation (Competition Contribution)},
    volume = {13244},
    year = {2022}
}

2021

[4] Hernán Ponce de León and Johannes Kinder. Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks. Tech. rep. arXiv:2108.13818, arXiv, 2021. BibTeX URL
@techreport{cats-vs-spectre-arxiv,
    author = {Hern{\'a}n Ponce de Le{\'o}n and Johannes Kinder},
    institution = {arXiv},
    number = {arXiv:2108.13818},
    title = {Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks},
    url = {https://arxiv.org/abs/2108.13818},
    year = {2021}
}

[5] Blake Loring and Johannes Kinder. Systematic Generation of Conformance Tests for JavaScript. Tech. rep. arXiv:2108.07075, arXiv, 2021. BibTeX URL
@techreport{conformance-testing-arxiv,
    author = {Blake Loring and Johannes Kinder},
    institution = {arXiv},
    number = {arXiv:2108.07075},
    title = {Systematic Generation of Conformance Tests for JavaScript},
    url = {https://arxiv.org/abs/2108.07075},
    year = {2021}
}

[6] James Patrick-Evans, Moritz Dannehl, and Johannes Kinder. XFL: eXtreme Function Labeling. Tech. rep. arXiv:2107.13404, arXiv, 2021. BibTeX URL
@techreport{xfl-arxiv,
    author = {James Patrick-Evans and Moritz Dannehl and Johannes Kinder},
    institution = {arXiv},
    number = {arXiv:2107.13404},
    title = {XFL: eXtreme Function Labeling},
    url = {https://arxiv.org/abs/2107.13404},
    year = {2021}
}

[7] Hernán Ponce de León, Thomas Hass, and Roland Meyer. Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution). In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 428–432, Springer, 2021. BibTeX PDF
@inproceedings{tacas21-dartagnan,
    author = {Hern{\'a}n Ponce de Le{\'o}n and Thomas Hass and Roland Meyer},
    booktitle = {Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
    pages = {428--432},
    publisher = {Springer},
    series = {LNCS},
    title = {Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution)},
    volume = {12652},
    year = {2021}
}

2020

[8] James Patrick-Evans, Lorenzo Cavallaro, and Johannes Kinder. Probabilistic Naming of Functions in Stripped Binaries. In Proc. 35th Annu. Computer Security Applications Conference (ACSAC), pp. 373–385, ACM, 2020. BibTeX PDF
@inproceedings{acsac20-punstrip,
    author = {James Patrick-Evans and Lorenzo Cavallaro and Johannes Kinder},
    booktitle = {Proc. 35th Annu. Computer Security Applications Conference (ACSAC)},
    doi = {10.1145/3427228.3427265},
    pages = {373--385},
    publisher = {ACM},
    title = {Probabilistic Naming of Functions in Stripped Binaries},
    year = {2020}
}

[9] Daniel Lehmann, Johannes Kinder, and Michael Pradel. Everything Old is New Again: Binary Security of WebAssembly. In 29th USENIX Security Symposium (USENIX Security), pp. 217–234, USENIX Association, 2020. BibTeX PDF
@inproceedings{usenixsecurity20-wasm,
    author = {Daniel Lehmann and Johannes Kinder and Michael Pradel},
    booktitle = {29th USENIX Security Symposium (USENIX Security)},
    pages = {217--234},
    publisher = {USENIX Association},
    title = {Everything Old is New Again: Binary Security of WebAssembly},
    year = {2020}
}

[10] Hernán Ponce de León, Florian Furbach, Keijo Heljanko, and Roland Meyer. Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution). In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 378–382, Springer, 2020. BibTeX PDF
@inproceedings{tacas20-dartagnan,
    author = {Hern{\'a}n Ponce de Le{\'o}n and Florian Furbach and Keijo Heljanko and Roland Meyer},
    booktitle = {Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
    pages = {378--382},
    publisher = {Springer},
    series = {LNCS},
    title = {Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)},
    volume = {12079},
    year = {2020}
}

[11] Pierre Bouvier, Hubert Garavel, and Hernán Ponce de León. Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account. In Proc. 41st Int. Conf. Application and Theory of Petri Nets and Concurrency (Petri Nets), pp. 3–23, Springer, 2020. BibTeX PDF
@inproceedings{petrinets20,
    author = {Pierre Bouvier and Hubert Garavel and Hern{\'a}n Ponce de Le{\'o}n},
    booktitle = {Proc. 41st Int. Conf. Application and Theory of Petri Nets and Concurrency (Petri Nets)},
    pages = {3--23},
    publisher = {Springer},
    series = {LNCS},
    title = {Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account},
    volume = {12152},
    year = {2020}
}

2019

[12] Lorenzo Cavallaro, Johannes Kinder, XiaoFeng Wang, and Jonathan Katz (eds). Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019. ACM, 2019. BibTeX URL
@proceedings{ccs2019,
    doi = {10.1145/3319535},
    editor = {Lorenzo Cavallaro and Johannes Kinder and XiaoFeng Wang and Jonathan Katz},
    isbn = {978-1-4503-6747-9},
    publisher = {ACM},
    title = {Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019},
    url = {https://dl.acm.org/doi/proceedings/10.1145/3319535},
    year = {2019}
}

[13] Duncan Mitchell and Johannes Kinder. A Formal Model for Checking Cryptographic API Usage in JavaScript. In Proc. European Symposium on Research in Computer Security (ESORICS), pp. 341–360, Springer, 2019. BibTeX PDF
@inproceedings{esorics19-secannjs,
    author = {Duncan Mitchell and Johannes Kinder},
    booktitle = {Proc. European Symposium on Research in Computer Security (ESORICS)},
    pages = {341--360},
    publisher = {Springer},
    series = {LNCS},
    title = {A Formal Model for Checking Cryptographic API Usage in JavaScript},
    volume = {11735},
    year = {2019}
}

[14] Feargus Pendlebury, Fabio Pierazzi, Roberto Jordaney, Johannes Kinder, and Lorenzo Cavallaro. TESSERACT: Eliminating Experimental Bias in Malware Classification across Space and Time. In 28th USENIX Security Symposium (USENIX Security), pp. 729–746, USENIX Association, 2019. BibTeX PDF
@inproceedings{usenixsecurity19-tesseract,
    author = {Feargus Pendlebury and Fabio Pierazzi and Roberto Jordaney and Johannes Kinder and Lorenzo Cavallaro},
    booktitle = {28th USENIX Security Symposium (USENIX Security)},
    pages = {729--746},
    publisher = {USENIX Association},
    title = {TESSERACT: Eliminating Experimental Bias in Malware Classification across Space and Time},
    year = {2019}
}

[15] Blake Loring, Duncan Mitchell, and Johannes Kinder. Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript. In Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), pp. 425–438, ACM, 2019. BibTeX PDF
@inproceedings{pldi19-regex,
    author = {Blake Loring and Duncan Mitchell and Johannes Kinder},
    booktitle = {Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI)},
    pages = {425--438},
    publisher = {ACM},
    title = {Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript},
    year = {2019}
}

2018

[16] Blake Loring, Duncan Mitchell, and Johannes Kinder. Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript. Tech. rep. CoRR:abs/1810.05661, arXiv, 2018. BibTeX URL
@techreport{regex-arxiv,
    author = {Blake Loring and Duncan Mitchell and Johannes Kinder},
    institution = {arXiv},
    number = {CoRR:abs/1810.05661},
    title = {Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript},
    url = {https://arxiv.org/abs/1810.05661},
    year = {2018}
}

[17] Feargus Pendlebury, Fabio Pierazzi, Roberto Jordaney, Johannes Kinder, and Lorenzo Cavallaro. TESSERACT: Eliminating Experimental Bias in Malware Classification across Space and Time. Tech. rep. CoRR:abs/1807.07838, arXiv, 2018. BibTeX URL
@techreport{tesseract-arxiv,
    author = {Feargus Pendlebury and Fabio Pierazzi and Roberto Jordaney and Johannes Kinder and Lorenzo Cavallaro},
    institution = {arXiv},
    number = {CoRR:abs/1807.07838},
    title = {TESSERACT: Eliminating Experimental Bias in Malware Classification across Space and Time},
    url = {https://arxiv.org/abs/1807.07838},
    year = {2018}
}

[18] Feargus Pendlebury, Fabio Pierazzi, Roberto Jordaney, Johannes Kinder, and Lorenzo Cavallaro. Enabling Fair ML Evaluations for Security. In Proc. 2018 ACM SIGSAC Conf. Computer and Communications Security (CCS), pp. 2264–2266, 2018. BibTeX PDF
@inproceedings{ccs18poster,
    author = {Feargus Pendlebury and Fabio Pierazzi and Roberto Jordaney and Johannes Kinder and Lorenzo Cavallaro},
    booktitle = {Proc. 2018 ACM SIGSAC Conf. Computer and Communications Security (CCS)},
    pages = {2264--2266},
    title = {Enabling Fair ML Evaluations for Security},
    year = {2018}
}

[19] Claudio Rizzo, Lorenzo Cavallaro, and Johannes Kinder. BabelView: Evaluating the Impact of Code Injection Attacks in Mobile Webviews. In Int. Symp. Research in Attacks, Intrusions, and Defenses (RAID), 2018. BibTeX PDF
@inproceedings{raid18-babelview,
    author = {Claudio Rizzo and Lorenzo Cavallaro and Johannes Kinder},
    booktitle = {Int. Symp. Research in Attacks, Intrusions, and Defenses (RAID)},
    title = {BabelView: Evaluating the Impact of Code Injection Attacks in Mobile Webviews},
    year = {2018}
}

[20] Duncan Mitchell, L. Thomas van Binsbergen, Blake Loring, and Johannes Kinder. Checking Cryptographic API Usage with Composable Annotations. In ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), 2018. BibTeX PDF
@inproceedings{pepm18-security-annotations,
    author = {Duncan Mitchell and L. Thomas van Binsbergen and Blake Loring and Johannes Kinder},
    booktitle = {ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM)},
    title = {Checking Cryptographic API Usage with Composable Annotations},
    year = {2018}
}

2017

[21] Claudio Rizzo, Lorenzo Cavallaro, and Johannes Kinder. BabelView: Evaluating the Impact of Code Injection Attacks in Mobile Webviews. Tech. rep. CoRR:abs/1709.05690, arXiv, 2017. BibTeX URL
@techreport{babelview-arxiv,
    author = {Claudio Rizzo and Lorenzo Cavallaro and Johannes Kinder},
    institution = {arXiv},
    number = {CoRR:abs/1709.05690},
    title = {BabelView: Evaluating the Impact of Code Injection Attacks in Mobile Webviews},
    url = {https://arxiv.org/abs/1709.05690},
    year = {2017}
}

[22] Dusan Repel, Johannes Kinder, and Lorenzo Cavallaro. Modular Synthesis of Heap Exploits. In Proc. ACM SIGSAC Workshop on Programming Languages and Analysis for Security (PLAS), 2017. BibTeX PDF
@inproceedings{plas17,
    author = {Dusan Repel and Johannes Kinder and Lorenzo Cavallaro},
    booktitle = {Proc. ACM SIGSAC Workshop on Programming Languages and Analysis for Security (PLAS)},
    title = {Modular Synthesis of Heap Exploits},
    year = {2017}
}

[23] James Patrick-Evans, Lorenzo Cavallaro, and Johannes Kinder. POTUS: Probing Off-The-Shelf USB Drivers with Symbolic Fault Injection. In 11th USENIX Workshop on Offensive Technologies (WOOT), 2017. Best Paper Award. BibTeX PDF
@inproceedings{woot17-potus,
    author = {James Patrick-Evans and Lorenzo Cavallaro and Johannes Kinder},
    booktitle = {11th USENIX Workshop on Offensive Technologies (WOOT)},
    note = {Best Paper Award},
    title = {POTUS: Probing Off-The-Shelf USB Drivers with Symbolic Fault Injection},
    year = {2017}
}

[24] Blake Loring, Duncan Mitchell, and Johannes Kinder. ExpoSE: Practical Symbolic Execution of Standalone JavaScript. In Proc. Int. SPIN Symp. Model Checking of Software (SPIN), pp. 196–199, ACM, 2017. BibTeX PDF
@inproceedings{spin17-expose,
    author = {Blake Loring and Duncan Mitchell and Johannes Kinder},
    booktitle = {Proc. Int. SPIN Symp. Model Checking of Software (SPIN)},
    pages = {196--199},
    publisher = {ACM},
    title = {ExpoSE: Practical Symbolic Execution of Standalone JavaScript},
    year = {2017}
}

[25] Guillermo Suarez-Tangil, Santanu Kumar Dash, Mansour Ahmadi, Johannes Kinder, Giorgio Giacinto, and Lorenzo Cavallaro. DroidSieve: Fast and Accurate Classification of Obfuscated Android Malware. In Proc. 7th ACM Conf. Data and Application Security and Privacy (CODASPY), pp. 309–320, ACM, 2017. BibTeX PDF
@inproceedings{codaspy17-droidsieve,
    author = {Guillermo Suarez-Tangil and Santanu Kumar Dash and Mansour Ahmadi and Johannes Kinder and Giorgio Giacinto and Lorenzo Cavallaro},
    booktitle = {Proc. 7th ACM Conf. Data and Application Security and Privacy (CODASPY)},
    pages = {309--320},
    publisher = {ACM},
    title = {DroidSieve: Fast and Accurate Classification of Obfuscated Android Malware},
    year = {2017}
}

2016

[26] Santanu Kumar Dash, Kimberly Tam, Johannes Kinder, and Lorenzo Cavallaro. Barometer: Sizing Up Android Applications Through Statistical Evaluation. In 37th IEEE Symp. Security and Privacy (S&P), May 2016. Poster. BibTeX
@conference{sp16poster,
    author = {Santanu Kumar Dash and Kimberly Tam and Johannes Kinder and Lorenzo Cavallaro},
    booktitle = {37th IEEE Symp. Security and Privacy (S\&P)},
    month = {May},
    note = {Poster},
    title = {Barometer: Sizing Up Android Applications Through Statistical Evaluation},
    year = {2016}
}

[27] Sebastian Schrittwieser, Stefan Katzenbeisser, Johannes Kinder, Georg Merzdovnik, and Edgar Weippl. Protecting Software through Obfuscation: Can It Keep Pace with Progress in Code Analysis? ACM Computing Surveys, 49(1):April 2016. BibTeX PDF
@article{csur16-obfuscation,
    author = {Sebastian Schrittwieser and Stefan Katzenbeisser and Johannes Kinder and Georg Merzdovnik and Edgar Weippl},
    journal = {ACM Computing Surveys},
    month = {April},
    number = {1},
    title = {Protecting Software through Obfuscation: Can It Keep Pace with Progress in Code Analysis?},
    volume = {49},
    year = {2016}
}

[28] Santanu Kumar Dash, Guillermo Suarez-Tangil, Salahuddin Khan, Kimberly Tam, Mansour Ahmadi, Johannes Kinder, and Lorenzo Cavallaro. DroidScribe: Classifying Android Malware Based on Runtime Behavior. In Proc. IEEE Symp. Security and Privacy Workshops (SPW), Mobile Security Technologies (MoST), pp. 252–261, 2016. BibTeX PDF
@inproceedings{most16-droidscribe,
    author = {Santanu Kumar Dash and Guillermo Suarez-Tangil and Salahuddin Khan and Kimberly Tam and Mansour Ahmadi and Johannes Kinder and Lorenzo Cavallaro},
    booktitle = {Proc. IEEE Symp. Security and Privacy Workshops (SPW), Mobile Security Technologies (MoST)},
    pages = {252--261},
    title = {DroidScribe: Classifying Android Malware Based on Runtime Behavior},
    year = {2016}
}

2015

[29] Santanu Kumar Dash, Kimberly Tam, Johannes Kinder, and Lorenzo Cavallaro. Set-based Classification of Android Malware from Behavioral Abstractions. In 24th USENIX Security Symp. (USENIX Security), August 2015. Poster. BibTeX
@conference{usenix15poster,
    author = {Santanu Kumar Dash and Kimberly Tam and Johannes Kinder and Lorenzo Cavallaro},
    booktitle = {24th USENIX Security Symp. (USENIX Security)},
    month = {August},
    note = {Poster},
    title = {Set-based Classification of Android Malware from Behavioral Abstractions},
    year = {2015}
}

[30] Jonas Wagner, Volodymyr Kuznetsov, George Candea, and Johannes Kinder. High System-Code Security with Low Overhead. In Proc. IEEE Symp. Security and Privacy (S&P), pp. 866–879, IEEE, 2015. BibTeX PDF
@inproceedings{oakland15,
    author = {Jonas Wagner and Volodymyr Kuznetsov and George Candea and Johannes Kinder},
    booktitle = {Proc. IEEE Symp. Security and Privacy (S\&P)},
    pages = {866--879},
    publisher = {IEEE},
    title = {High System-Code Security with Low Overhead},
    year = {2015}
}

[31] Johannes Kinder. Hypertesting: The Case for Automated Testing of Hyperproperties. In 3rd Workshop on Hot Issues in Security Principles and Trust (HotSpot), pp. 1–8, 2015. BibTeX PDF
@inproceedings{hotspot15,
    author = {Johannes Kinder},
    booktitle = {3rd Workshop on Hot Issues in Security Principles and Trust (HotSpot)},
    pages = {1--8},
    title = {Hypertesting: The Case for Automated Testing of Hyperproperties},
    year = {2015}
}

[32] Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea. Advantageous State Merging During Symbolic Analysis. Pat. US 9,141,354 B2, September 2015. Issued. BibTeX
@patent{statemerging-patent,
    author = {Volodymyr Kuznetsov and Johannes Kinder and Stefan Bucur and George Candea},
    month = {September},
    number = {US 9,141,354 B2},
    pubstate = {Issued},
    title = {Advantageous State Merging During Symbolic Analysis},
    year = {2015}
}

2014

[33] Jonas Wagner, Volodymyr Kuznetsov, Johannes Kinder, Azqa Nadeem, and George Candea. ASAP: High Security at Low Overhead. In 11th USENIX Symp. Operating Systems Design and Implementation (OSDI), October 2014. Poster. BibTeX
@conference{osdi14poster,
    author = {Jonas Wagner and Volodymyr Kuznetsov and Johannes Kinder and Azqa Nadeem and George Candea},
    booktitle = {11th USENIX Symp. Operating Systems Design and Implementation (OSDI)},
    month = {October},
    note = {Poster},
    title = {ASAP: High Security at Low Overhead},
    year = {2014}
}

[34] Stefan Bucur, Johannes Kinder, and George Candea. Prototyping Symbolic Execution Engines for Interpreted Languages. In Proc. 19th Int. Conf. Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 239–254, ACM, 2014. BibTeX PDF
@inproceedings{asplos14,
    author = {Stefan Bucur and Johannes Kinder and George Candea},
    booktitle = {Proc. 19th Int. Conf. Architectural Support for Programming Languages and Operating Systems (ASPLOS)},
    doi = {10.1145/2541940.2541977},
    pages = {239--254},
    publisher = {ACM},
    title = {Prototyping Symbolic Execution Engines for Interpreted Languages},
    year = {2014}
}

[35] Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea. Efficient State Merging in Symbolic Execution (Extended Abstract). In Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik (SE), pp. 45–46, GI, 2014. BibTeX
@inproceedings{se14,
    author = {Volodymyr Kuznetsov and Johannes Kinder and Stefan Bucur and George Candea},
    booktitle = {Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik (SE)},
    pages = {45--46},
    publisher = {GI},
    series = {LNI},
    title = {Efficient State Merging in Symbolic Execution (Extended Abstract)},
    volume = {227},
    year = {2014}
}

[36] Patrice Godefroid and Johannes Kinder. Memory Safety of Floating-Point Computations. Pat. US 8,782,625 B2, July 2014. Issued. BibTeX
@patent{fpsafety-patent,
    author = {Patrice Godefroid and Johannes Kinder},
    month = {July},
    number = {US 8,782,625 B2},
    pubstate = {Issued},
    title = {Memory Safety of Floating-Point Computations},
    year = {2014}
}

2013

[37] Stefan Bucur, Johannes Kinder, and George Candea. Making Automated Testing of Cloud Applications an Integral Component of PaaS. In Proc. 4th Asia-Pacific Workshop on Systems (APSYS), pp. 18:1–18:7, ACM, 2013. BibTeX PDF
@inproceedings{apsys13,
    author = {Stefan Bucur and Johannes Kinder and George Candea},
    booktitle = {Proc. 4th Asia-Pacific Workshop on Systems (APSYS)},
    doi = {10.1145/2500727.2500730},
    pages = {18:1--18:7},
    publisher = {ACM},
    title = {Making Automated Testing of Cloud Applications an Integral Component of PaaS},
    year = {2013}
}

[38] Cristian Zamfir, Baris Kasikci, Johannes Kinder, Edouard Bugnion, and George Candea. Automated Debugging for Arbitrarily Long Executions. In Proc. 14th Workshop on Hot Topics in Operating Systems (HotOS), USENIX, 2013. BibTeX PDF
@inproceedings{hotos13,
    author = {Cristian Zamfir and Baris Kasikci and Johannes Kinder and Edouard Bugnion and George Candea},
    booktitle = {Proc. 14th Workshop on Hot Topics in Operating Systems (HotOS)},
    ee = {https://www.usenix.org/conference/hotos13/session/zamfir},
    publisher = {USENIX},
    title = {Automated Debugging for Arbitrarily Long Executions},
    year = {2013}
}

2012

[39] Stefan Bucur, Johannes Kinder, and George Candea. C3A: Client/Server Co-Verification for Cloud Applications. In 10th USENIX Symp. Operating Systems Design and Implementation (OSDI), October 2012. Poster. BibTeX
@conference{osdi12poster,
    author = {Stefan Bucur and Johannes Kinder and George Candea},
    booktitle = {10th USENIX Symp. Operating Systems Design and Implementation (OSDI)},
    month = {October},
    note = {Poster},
    title = {C3A: Client/Server Co-Verification for Cloud Applications},
    year = {2012}
}

[40] Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea. Efficient state merging in symbolic execution. In Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), pp. 193–204, ACM, 2012. BibTeX PDF
@inproceedings{pldi12,
    author = {Volodymyr Kuznetsov and Johannes Kinder and Stefan Bucur and George Candea},
    booktitle = {Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI)},
    pages = {193--204},
    publisher = {ACM},
    title = {Efficient state merging in symbolic execution},
    year = {2012}
}

[41] Johannes Kinder. Towards Static Analysis of Virtualization-Obfuscated Binaries. In Proc. 19th Working Conf. Reverse Engineering (WCRE), pp. 61–70, IEEE, 2012. BibTeX PDF
@inproceedings{wcre12,
    author = {Johannes Kinder},
    booktitle = {Proc. 19th Working Conf. Reverse Engineering (WCRE)},
    pages = {61--70},
    publisher = {IEEE},
    title = {Towards Static Analysis of Virtualization-Obfuscated Binaries},
    year = {2012}
}

[42] Johannes Kinder and Dmitry Kravchenko. Alternating Control Flow Reconstruction. In Proc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 267–282, Springer, 2012. BibTeX PDF
@inproceedings{vmcai12,
    author = {Johannes Kinder and Dmitry Kravchenko},
    booktitle = {Proc. 13th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI)},
    pages = {267--282},
    publisher = {Springer},
    series = {LNCS},
    title = {Alternating Control Flow Reconstruction},
    volume = {7148},
    year = {2012}
}

2011

[43] Péter Bokor, Johannes Kinder, Marco Serafini, and Neeraj Suri. Supporting domain-specific state space reductions through local partial-order reduction. In 26th IEEE/ACM Int. Conf. Automated Software Engineering (ASE), pp. 113–122, IEEE, 2011. BibTeX PDF
@inproceedings{ase11,
    author = {P{\'e}ter Bokor and Johannes Kinder and Marco Serafini and Neeraj Suri},
    booktitle = {26th IEEE/ACM Int. Conf. Automated Software Engineering (ASE)},
    pages = {113--122},
    publisher = {IEEE},
    title = {Supporting domain-specific state space reductions through local partial-order reduction},
    year = {2011}
}

[44] Péter Bokor, Johannes Kinder, Marco Serafini, and Neeraj Suri. Efficient model checking of fault-tolerant distributed protocols. In Proc. 2011 IEEE/IFIP Int. Conf. Dependable Systems and Networks (DSN), pp. 73–84, IEEE, 2011. BibTeX PDF
@inproceedings{dsn11,
    author = {P{\'e}ter Bokor and Johannes Kinder and Marco Serafini and Neeraj Suri},
    booktitle = {Proc. 2011 IEEE/IFIP Int. Conf. Dependable Systems and Networks (DSN)},
    pages = {73--84},
    publisher = {IEEE},
    title = {Efficient model checking of fault-tolerant distributed protocols},
    year = {2011}
}

[45] Stefan Katzenbeisser, Johannes Kinder, and Helmut Veith. Malware Detection. In Henk C. A. van Tilborg and Sushil Jajodia, eds., Encyclopedia of Cryptography and Security (2nd Ed.), pp. 752–755, Springer, 2011. BibTeX
@incollection{cryptosec11,
    author = {Stefan Katzenbeisser and Johannes Kinder and Helmut Veith},
    booktitle = {Encyclopedia of Cryptography and Security (2nd Ed.)},
    editor = {Henk C. A. van Tilborg and Sushil Jajodia},
    pages = {752--755},
    publisher = {Springer},
    title = {Malware Detection},
    year = {2011}
}

[46] Péter Bokor, Johannes Kinder, Marco Serafini, and Neeraj Suri. Supporting domain-specific state space reductions through local partial-order reduction. Tech. rep. TR-TUD-DEEDS-07-01-2011, Technische Universität Darmstadt, 2011. BibTeX
@techreport{lpor-tr,
    author = {P{\'e}ter Bokor and Johannes Kinder and Marco Serafini and Neeraj Suri},
    institution = {Technische Universit{\"a}t Darmstadt},
    number = {TR-TUD-DEEDS-07-01-2011},
    title = {Supporting domain-specific state space reductions through local partial-order reduction},
    year = {2011}
}

[47] Péter Bokor, Johannes Kinder, Marco Serafini, and Neeraj Suri. Efficient model checking of fault-tolerant distributed protocols. Tech. rep. TR-TUD-DEEDS-01-01-2011, Technische Universität Darmstadt, 2011. BibTeX
@techreport{mpbasset-tr,
    author = {P{\'e}ter Bokor and Johannes Kinder and Marco Serafini and Neeraj Suri},
    institution = {Technische Universit{\"a}t Darmstadt},
    number = {TR-TUD-DEEDS-01-01-2011},
    title = {Efficient model checking of fault-tolerant distributed protocols},
    year = {2011}
}

2010

[48] Johannes Kinder. Static Analysis of x86 Executables. Ph.D. Thesis, Technische Universität Darmstadt, 2010. BibTeX PDF
@phdthesis{phdthesis,
    author = {Johannes Kinder},
    school = {Technische Universit{\"a}t Darmstadt},
    title = {Static Analysis of x86 Executables},
    year = {2010}
}

[49] Johannes Kinder and Helmut Veith. Precise Static Analysis of Untrusted Driver Binaries. In Proc. 10th Int. Conf. Formal Methods in Computer-Aided Design (FMCAD), pp. 43–50, 2010. BibTeX PDF
@inproceedings{fmcad10,
    author = {Johannes Kinder and Helmut Veith},
    booktitle = {Proc. 10th Int. Conf. Formal Methods in Computer-Aided Design (FMCAD)},
    pages = {43--50},
    title = {Precise Static Analysis of Untrusted Driver Binaries},
    year = {2010}
}

[50] Patrice Godefroid and Johannes Kinder. Proving memory safety of floating-point computations by combining static and dynamic program analysis. In Proc. 19th Int. Symp. Software Testing and Analysis (ISSTA), pp. 1–12, ACM, 2010. BibTeX PDF
@inproceedings{issta10,
    author = {Patrice Godefroid and Johannes Kinder},
    booktitle = {Proc. 19th Int. Symp. Software Testing and Analysis (ISSTA)},
    doi = {10.1145/1831708.1831710},
    pages = {1--12},
    publisher = {ACM},
    title = {Proving memory safety of floating-point computations by combining static and dynamic program analysis},
    year = {2010}
}

[51] Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, and Helmut Veith. Proactive Detection of Computer Worms Using Model Checking. IEEE Trans. Dependable Sec. Comput., 7(4):424–438, October 2010. BibTeX PDF
@article{tdsc10,
    author = {Johannes Kinder and Stefan Katzenbeisser and Christian Schallhart and Helmut Veith},
    journal = {IEEE Trans. Dependable Sec. Comput.},
    month = {October},
    number = {4},
    pages = {424--438},
    title = {Proactive Detection of Computer Worms Using Model Checking},
    volume = {7},
    year = {2010}
}

[52] Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, and Helmut Veith. System for Malware Normalization and Detection. Pat. US 2010/0011441 A1, January 2010. Published. BibTeX
@patent{malwarenorm-patent,
    author = {Mihai Christodorescu and Johannes Kinder and Somesh Jha and Stefan Katzenbeisser and Helmut Veith},
    month = {January},
    number = {US 2010/0011441 A1},
    pubstate = {Published},
    title = {System for Malware Normalization and Detection},
    year = {2010}
}

2009

[53] Patrice Godefroid and Johannes Kinder. Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis. Tech. rep. MSR-TR-2009-167, Microsoft Research, November 2009. BibTeX
@techreport{fpsafety-tr,
    author = {Patrice Godefroid and Johannes Kinder},
    institution = {Microsoft Research},
    month = {November},
    number = {MSR-TR-2009-167},
    title = {Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis},
    year = {2009}
}

[54] Johannes Kinder, Helmut Veith, and Florian Zuleger. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. In Proc. 10th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 214–228, Springer, 2009. BibTeX PDF
@inproceedings{vmcai09,
    author = {Johannes Kinder and Helmut Veith and Florian Zuleger},
    booktitle = {Proc. 10th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI)},
    pages = {214--228},
    publisher = {Springer},
    series = {LNCS},
    title = {An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries},
    volume = {5403},
    year = {2009}
}

2008

[55] Johannes Kinder and Helmut Veith. Jakstab: A Static Analysis Platform for Binaries. In Proc. 20th Int. Conf. Computer Aided Verification (CAV), pp. 423–427, Springer, 2008. BibTeX PDF
@inproceedings{cav08,
    author = {Johannes Kinder and Helmut Veith},
    booktitle = {Proc. 20th Int. Conf. Computer Aided Verification (CAV)},
    booktitleshort = {CAV},
    pages = {423--427},
    publisher = {Springer},
    series = {LNCS},
    title = {Jakstab: A Static Analysis Platform for Binaries},
    volume = {5123},
    year = {2008}
}

2007

[56] Mihai Christodorescu, Somesh Jha, Johannes Kinder, Stefan Katzenbeisser, and Helmut Veith. Software transformations to improve malware detection. J. Comput. Virol., 3(4):253–265, November 2007. BibTeX PDF
@article{jicv07,
    author = {Mihai Christodorescu and Somesh Jha and Johannes Kinder and Stefan Katzenbeisser and Helmut Veith},
    doi = {10.1007/s11416-007-0059-8},
    journal = {J. Comput. Virol.},
    month = {November},
    number = {4},
    pages = {253--265},
    title = {Software transformations to improve malware detection},
    volume = {3},
    year = {2007}
}

[57] Andreas Holzer, Johannes Kinder, and Helmut Veith. Using Verification Technology to Specify and Detect Malware. In Proc. 11th Int. Conf. Computer Aided Systems Theory (EUROCAST), pp. 497–504, Springer, 2007. BibTeX PDF
@inproceedings{eurocast07,
    author = {Andreas Holzer and Johannes Kinder and Helmut Veith},
    booktitle = {Proc. 11th Int. Conf. Computer Aided Systems Theory (EUROCAST)},
    pages = {497--504},
    publisher = {Springer},
    series = {LNCS},
    title = {Using Verification Technology to Specify and Detect Malware},
    volume = {4739},
    year = {2007}
}

2005

[58] Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, and Helmut Veith. Malware Normalization. Tech. rep. 1539, University of Wisconsin, November 2005. BibTeX PDF
@techreport{malwarenorm,
    address = {Madison, WI, USA},
    author = {Mihai Christodorescu and Johannes Kinder and Somesh Jha and Stefan Katzenbeisser and Helmut Veith},
    institution = {University of Wisconsin},
    month = {November},
    number = {1539},
    title = {Malware Normalization},
    year = {2005}
}

[59] Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, and Helmut Veith. Detecting Malicious Code by Model Checking. In Second Int. Conf. Detection of Intrusions and Malware & Vulnerability Assessment (DIMVA), pp. 174–187, Springer, 2005. BibTeX PDF
@inproceedings{dimva05,
    author = {Johannes Kinder and Stefan Katzenbeisser and Christian Schallhart and Helmut Veith},
    booktitle = {Second Int. Conf. Detection of Intrusions and Malware \& Vulnerability Assessment (DIMVA)},
    pages = {174--187},
    publisher = {Springer},
    series = {LNCS},
    title = {Detecting Malicious Code by Model Checking},
    volume = {3548},
    year = {2005}
}

[60] Johannes Kinder. Model Checking Malicious Code. M.Sc. Thesis, Technische Universität München, 2005. BibTeX PDF
@thesis{da-kinder,
    author = {Johannes Kinder},
    school = {Technische Universit{\"a}t M{\"u}nchen},
    title = {Model Checking Malicious Code},
    type = {MSc thesis},
    year = {2005}
}