@inproceedings{usenixsecurity19-tesseract,
  author    = {Feargus Pendlebury and Fabio Pierazzi and Roberto Jordaney and Johannes Kinder and Lorenzo Cavallaro},
  title     = {{TESSERACT}: Eliminating Experimental Bias in Malware Classification across Space and Time},
  booktitle = {USENIX Security Symposium},
  year      = 2019,
  publisher = {USENIX Association},
  note      = {To appear},
}

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

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

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

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

@inproceedings{spin17-expose,
  author    = {Blake Loring and Duncan Mitchell and Johannes Kinder},
  title     = {{ExpoSE}: Practical Symbolic Execution of Standalone {JavaScript}},
  booktitle = {Proc. Int. SPIN Symp. Model Checking of Software (SPIN)},
  pages     = {196-199},
  publisher = {ACM},
  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},
  title     = {{DroidSieve}: Fast and Accurate Classification of Obfuscated Android Malware},
  booktitle = {Proc. 7th ACM Conf. Data and Application Security
               and Privacy (CODASPY)},
  pages     = {309-320},
  publisher = {ACM},
  year      = 2017,
}

@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},
  title     = {{DroidScribe}: Classifying Android Malware Based on Runtime Behavior},
  booktitle = {Proc. IEEE Symp. Security and Privacy Workshops (SPW), Mobile Security Technologies (MoST)},
  year      = 2016,
  pages     = {252-261},
}

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

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

@inproceedings{asplos14,
  author    = {Stefan Bucur and
               Johannes Kinder and
               George Candea},
  title     = {Prototyping Symbolic Execution Engines for Interpreted Languages},
  booktitle = {Proc. 19th Int. Conf. Architectural Support for Programming 
               Languages and Operating Systems (ASPLOS)},
  pages     = {239-254},
  ee        = {http://doi.acm.org/10.1145/2541940.2541977},
  publisher = {ACM},
  year      = 2014,
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@article{jicv07,
  author    = {Mihai Christodorescu and
               Somesh Jha and
               Johannes Kinder and
               Stefan Katzenbeisser and
               Helmut Veith},
  title     = {Software transformations to improve malware detection},
  journal   = {J. Comput. Virol.},
  volume    = {3},
  number    = {4},
  year      = 2007,
  month     = nov,
  pages     = {253-265},
  ee        = {http://dx.doi.org/10.1007/s11416-007-0059-8},
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@techreport{malwarenorm,
  author      = {Mihai Christodorescu and Johannes Kinder and Somesh Jha and Stefan Katzenbeisser and Helmut Veith},
  title       = {Malware Normalization},
  institution = {University of Wisconsin},
  year        = 2005,
  number      = 1539,
  address     = {Madison, WI, USA},
  month       = nov,
}