Publications

2019

[1] 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
@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},
    year = {2019}
}

[2] 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)},
    doi = {10.1007/978-3-030-29959-0\_17},
    pages = {341--360},
    publisher = {Springer},
    series = {LNCS},
    title = {A Formal Model for Checking Cryptographic API Usage in JavaScript},
    volume = {11735},
    year = {2019}
}

[3] 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}
}

[4] 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

[5] 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
@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}
}

[6] 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
@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}
}

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

[8] 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}
}

[9] 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

[10] 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
@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}
}

[11] 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}
}

[12] 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}
}

[13] 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}
}

[14] 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

[15] 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}
}

[16] 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}
}

[17] 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

[18] 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}
}

[19] 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}
}

[20] 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}
}

[21] 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

[22] 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}
}

[23] 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)},
    ee = {http://doi.acm.org/10.1145/2541940.2541977},
    pages = {239--254},
    publisher = {ACM},
    title = {Prototyping Symbolic Execution Engines for Interpreted Languages},
    year = {2014}
}

[24] 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}
}

[25] 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

[26] 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)},
    ee = {http://doi.acm.org/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}
}

[27] 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

[28] 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}
}

[29] 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}
}

[30] 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}
}

[31] 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

[32] 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}
}

[33] 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}
}

[34] 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}
}

[35] 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}
}

[36] 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

[37] 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}
}

[38] 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}
}

[39] 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)},
    ee = {http://doi.acm.org/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}
}

[40] 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}
}

[41] 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

[42] 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}
}

[43] 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

[44] 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

[45] 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},
    ee = {http://dx.doi.org/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}
}

[46] 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

[47] 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}
}

[48] 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}
}

[49] 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}
}