@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@phdthesis{phdthesis,
    author = {Johannes Kinder},
    school = {Technische Universit{\"a}t Darmstadt},
    title = {Static Analysis of x86 Executables},
    year = {2010}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@thesis{da-kinder,
    author = {Johannes Kinder},
    school = {Technische Universit{\"a}t M{\"u}nchen},
    title = {Model Checking Malicious Code},
    type = {MSc thesis},
    year = {2005}
}