Felix Klaedtke

Senior Researcher
NEC Laboratories Europe
Address:
 
NEC Europe Ltd.
Kurfürsten-Anlage 36
69115 Heidelberg
Germany
                
Phone: +49 6221 4342-166
Email: felix.klaedtke_X_gmail.com (where _X_ actually means @)
PGP public key

Research Interests:

Monitoring, Model Checking, Verification, Building and Securing Software Systems, ...
If you want to know in more detail about my current research topics, or if you have questions about my former research, please do not hesitate to contact me.

Publications:

Journal Articles:

  1. First international competition on runtime verification: rules, benchmarks, tools and final results of CRV 2014.
    (co-authors: many)
    Accepted for publication at the International Journal of Software Tools for Technology Transfer.
    BibTeX DOI PDF (preprint) (coming soon)
  2. Algorithms for Monitoring Real-time Properties.
    (co-authors: David Basin and Eugen Zalinescu)
    Accepted for publication at Acta Informatica.
    BibTeX DOI PDF (preprint) (coming soon)
  3. On the Fingerprinting of Software-defined Networks.
    (co-authors: Roberto Bifulco, Heng Cui, and Ghassan O. Karame)
    IEEE Transactions of Information Forensics and Security, Volume 11, Issue 10, 2016.
    BibTeX DOI PDF (preprint) (coming soon)
  4. Scalable Offline Monitoring of Temporal Properties.
    (co-authors: David Basin, Germano Carroni, Sarah Ereth, Matus Harvan, and Heiko Mantel)
    Formal Methods in System Design, Volume 49, Issue 1-2, 2016. 
    BibTeX DOI PDF (preprint) (coming soon)
  5. Ramsey-based Inclusion Checking for Visibly Pushdown Automata.
    (co-authors: Oliver Friedmann and Martin Lange)
    ACM Transactions on Computational Logic, Volume 16, Issue 4, 2015.
    BibTeX DOI PDF (preprint)
  6. Monitoring Metric First-order Temporal Properties.
    (co-authors: David Basin, Samuel Mueller, and Eugen Zalinescu)
    Journal of the ACM, Volume 62, Issue 2, 2015.
    BibTeX  DOI  PDF (preprint)
  7. Monitoring of Temporal First-order Properties with Aggregations.
    (co-authors: David Basin, Srdjan Marinovic, and Eugen Zalinescu)
    Formal Methods in System Design, Volume 46, Issue 3, 2015.
    BibTeX  DOI  PDF (preprint)
  8. Greedily Computing Associative Aggregations on Sliding Windows.
    (co-authors: David Basin and Eugen Zalinescu)
    Information Processing Letters, Volume 115, Issue 2, 2015.
    BibTeX  DOI  PDF (preprint)  
    Supplementary material: OCaml code and Haskell code
  9. The mu-Calculus Alternation Hierarchy Collapses over Structures with Restricted Connectivity.
    (co-authors: Julian Gutierrez and Martin Lange)
    Theoretical Computer Science, Volume 560, Issue 3, 2014.
    BibTeX DOI  PDF (preprint)
  10. Deciding Safety and Liveness in TPTL.
    (co-authors: David Basin, Carlos Cotrini Jimenez, and Eugen Zalinescu)
    Information Processing Letters, Volume 114, Issue 12, 2014.
    BibTeX DOI PDF (preprint)
  11. Monitoring Data Usage in Distributed Systems.
    (co-authors: David Basin, Matus Harvan, and Eugen Zalinescu)
    IEEE Transactions on Software Engineering, Volume 39, Issue 10, 2013.
    BibTeX DOI PDF (preprint)
  12. Enforceable Security Policies Revisited.
    (co-authors: David Basin, Vincent Juge, and Eugen Zalinescu)
    ACM Transactions on Information and System Security, Volume 16, Issue 1, 2013.
    BibTeX DOI PDF (preprint)
  13. A Trace-based Model for Multiparty Contracts.
    (co-authors: Tom Hvitved and Eugen Zalinescu)
    The Journal of Logic and Algebraic Programming, Volume 81, Issue 2, 2012.
    BibTeX DOI PDF (preprint)
  14. Ehrenfeucht-Fraisse Goes Automatic for Real Addition.
    Information and Computation, Volume 208, Issue 11, 2010.
    BibTeX DOI PDF (preprint)
  15. On Regular Temporal Logics with Past.
    (co-authors: Christian Dax and Martin Lange)
    Acta Informatica, Volume 47, Issue 4, 2010.
    BibTeX DOI PDF (preprint)
  16. Don't Care Words with an Application to the Automata-Based Approach for Real Addition.
    (co-author: Jochen Eisinger)
    Formal Methods in System Design, Volume 33, Issue 1-3, 2008.
    BibTeX DOI PDF (preprint)
  17. Bounds on the Automata Size for Presburger Arithmetic.
    ACM Transactions on Computational Logic, Volume 9, Issue 2, 2008.
    BibTeX DOI PDF (preprint)
  18. Decision Procedures for Inductive Boolean Functions Based on Alternating Automata.
    (co-authors: Abdelwaheb Ayari and David Basin)
    Theoretical Computer Science, Volume 300, Issue 1-3, 2003.
    BibTeX DOI gzip'ed PostScript (preprint)

Conference Papers:

  1. Runtime Verification of Temporal Properties over Out-of-order Data Streams.
    (co-authors: David Basin and Eugen Zalinescu)
    Accepted for publication at the 29th International Conference on Computer Aided Verification (CAV 2017).
    BibTeX PDF PDF (full version) (coming soon)
  2. Failure-aware Runtime Verification of Distributed Systems.
    (co-authors: David Basin and Eugen Zalinescu)
    In the Proceedings of the 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015).
    BibTeX PDF PDF (full version) (coming soon)
  3. Scalable Offline Monitoring.
    (co-authors: David Basin, Germano Caronni, Sarah Ereth, Matus Harvan, and Heiko Mantel)
    In the Proceedings of the 5th International Conference on Runtime Verification (RV 2014).
    Volume 8734 of Lecture Notes in Computer Science, pages 31--47, Springer-Verlag, 2014.        
    BibTeX PDF PDF (full version)
    The original publication is available at www.springerlink.com.
  4. On Real-time Monitoring with Imprecise Timestamps.
    (co-authors: David Basin, Srdjan Marinovic, and Eugen Zalinescu)
    In the Proceedings of the 5th International Conference on Runtime Verification (RV 2014).
    Volume 8734 of Lecture Notes in Computer Science, pages 193--198, Springer-Verlag, 2014.          
    BibTeX PDF PDF (full version)
    The original publication is available at www.springerlink.com.
  5. Monitoring of Temporal First-order Properties with Aggregations.
    (co-authors: David Basin, Srdjan Marinovic, and Eugen Zalinescu)
    In the Proceedings of the 4th International Conference on Runtime Verification (RV 2013).
    Volume 8174 of Lecture Notes in Computer Science, pages 40--58, Springer-Verlag, 2013.
    BibTeX PDF
    The original publication is available at www.springerlink.com.
  6. Ramsey Goes Visibly Pushdown.
    (co-authors: Oliver Friedmann and Martin Lange)
    In the Proceedings of the 40th International Colloquium of Automata, Language and Programming (ICALP 2013).
    Volume 7966 of Lecture Notes in Computer Science, pages 224--237, Springer-Verlag, 2013.
    BibTeX PDF PDF (full version)
    The original publication is available at www.springerlink.com.
  7. Monitoring Compliance Policies over Incomplete and Disagreeing Logs.
    (co-authors: David Basin, Srdjan Marinovic, and Eugen Zalinescu)
    In the Proceedings of the 3rd International Conference on Runtime Verification (RV 2012).
    Volume 7687 of Lecture Notes in Computer Science, pages 151--167, Springer-Verlag, 2013.
    BibTeX PDF PDF (full version)
    The original publication is available at www.springerlink.com.
  8. The mu-Calculus Alternation Hierarchy Collapses over Structures with Restricted Connectivity.
    (co-authors: Julian Gutierrez and Martin Lange)
    In the Proceedings of the 3rd International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2012).
    Volume 96 of Electronic Proceedings in Theoretical Computer Science, pages 113--126, eptcs.org
    BibTeX PDF PDF (full version)
  9. Enforceable Security Policies Revisited.
    (co-authors: David Basin, Vincent Juge, and Eugen Zalinescu)
    In the Proceedings of the 1st Conference on Principles of Security and Trust (POST 2012).
    Volume 7215 of Lecture Notes in Computer Science, pages 309--328, Springer-Verlag, 2012.
    BibTeX PDF
    The original publication is available at www.springerlink.com.
  10. MONPOLY: Monitoring Usage-control Policies.
    (co-authors: David Basin, Matus Harvan, and Eugen Zalinescu)
    In the Proceedings of the 2nd International Conference on Runtime Verification (RV 2011).
    Volume 7186 of Lecture Notes in Computer Science, pages 360--364, Springer-Verlag, 2012.
    BibTeX PDF web page
    The original publication is available at www.springerlink.com.
  11. Algorithms for Monitoring Real-time Properties.
    (co-authors: David Basin and Eugen Zalinescu)
    In the Proceedings of the 2nd International Conference on Runtime Verification (RV 2011).
    Volume 7186 of Lecture Notes in Computer Science, pages 260--275, Springer-Verlag, 2012.
    BibTeX PDF PDF (full version)
    The original publication is available at www.springerlink.com.
  12. Monitoring Usage-control Policies in Distributed Systems.
    (co-authors: David Basin, Matus Harvan, and Eugen Zalinescu)
    In the Proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME 2011).
    Pages 88--95, IEEE Computer Society, 2011.
    BibTeX PDF PDF (full version)
  13. Alternation Elimination for Automata over Nested Words.
    (co-author: Christian Dax)
    In the Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2011).
    Volume 6604 of Lecture Notes in Computer Science, pages 168--183, Springer-Verlag, 2011.
    BibTeX PDF PDF (full version)
    The original publication is available at www.springerlink.com.
  14. Policy Monitoring in First-Order Temporal Logic.
    (co-authors: David Basin and Samuel Müller)
    In the Proceedings of the 22nd International Conference on Computer Aided Verification (CAV 2010).
    Volume 6174 of Lecture Notes in Computer Science, pages 1--18, Springer-Verlag, 2010.
    BibTeX PDF
  15. Monitoring Security Policies with Metric First-Order Temporal Logic.
    (co-authors: David Basin and Samuel Müller)
    In the Proceedings of the 15th ACM Symposium on Access Control Models and Technologies (SACMAT 2010).
    Pages 23--33, ACM Press, 2010.
    BibTeX PDF
  16. Specification Languages for Stutter-Invariant Regular Properties.
    (co-authors: Christian Dax and Stefan Leue)
    In the Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA 2009).
    Volume 5799 of Lecture Notes in Computer Science, pages 244--254, Springer-Verlag, 2009.
    BibTeX PDF
  17. On Regular Temporal Logics with Past.
    (co-authors: Christian Dax and Martin Lange)
    In the Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP 2009).
    Volume 5556 of Lecture nodes in Computer Science, pages 175--187, Springer-Verlag, 2009.
    BibTeX PDF PDF (full version)
  18. Runtime Monitoring of Metric First-order Temporal Properties.
    (co-authors: David Basin, Samuel Müller, and Birgit Pfitzmann)
    In the Proceedings of the 28th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008).
    Pages 49--60, IBFI Schloss Dagstuhl, 2008.
    BibTeX PDF PDF (full version)
  19. Alternation Elimination by Complementation.
    (co-author: Christian Dax)
    In the Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2008).
    Volume 5330 of Lecture Notes in Computer Science, pages 214--229, Springer-Verlag, 2008.
    BibTeX PDF PDF (full version)
  20. Ehrenfeucht-Fraisse Goes Automatic for Real Addition.
    In the Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS 2008).
    Pages 445--456, IBFI Schloss Dagstuhl, 2008.
    Available online at www.stacs-conf.org.
    BibTeX PDF PDF (full version)
  21. Mechanizing the Powerset Construction for Restricted Classes of omega-Automata.
    (co-authors: Christian Dax and Jochen Eisinger)
    In the Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007).
    Volume 4762 of Lecture Notes in Computer Science, pages 223--236, Springer-Verlag, 2007.
    BibTeX PDF
  22. LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals.
    (co-authors: Bernd Becker, Christian Dax, and Jochen Eisinger)
    In the Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007).
    Volume 4590 of Lecture Notes in Computer Science, pages 307--310. Springer-Verlag, 2007.
    BibTeX PDF
  23. Language-Based Abstraction Refinement for Hybrid System Verification.
    (co-authors: Stefan Ratschan and Zhikun She)
    In the Proceedings of the 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007).
    Volume 4349 of Lecture Notes in Computer Science, pages 151--166. Springer-Verlag, 2007.
    BibTeX PDF
  24. Don't Care Words with an Application to the Automata-based Approach for Real Addition.
    (co-author: Jochen Eisinger)
    In the Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006).
    Volume 4144 of Lecture Notes in Computer Science, pages 67--80. Springer-Verlag, 2006.
    BibTeX gzip'ed PostScript (with proof details)
  25. Optimizing Bounded Model Checking for Linear Hybrid Systems.
    (co-authors: Erika Abraham, Bernd Becker, and Martin Steffen)
    In the Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2005).
    Volume 3385 of Lecture Notes in Computer Science, pages 396--412. Springer-Verlag, 2005.
    BibTeX gzip'ed PostScript
  26. On the Automata Size for Presburger Arithmetic.
    In the Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004).
    Pages 110--119. IEEE Computer Society Press, 2004.
    BibTeX PDF (full version)
  27. Monadic Second-Order Logics with Cardinalities.
    (co-author: Harald Ruess)
    In the Proceedings of the 30th International Colloquium on Automata, Languages and Programming (ICALP 2003).
    Volume 2719 of Lecture Notes in Computer Science, pages 681--696. Springer-Verlag, 2003.
    BibTeX
  28. Decision Procedure for an Extension of WS1S.
    In the Proceedings of 10th Annual Conference of the EACSL (CSL 2001).
    Volume 2142 of Lecture Notes in Computer Science, pages 384--398. Springer-Verlag, 2001.
    BibTeX
  29. Decision Procedures for Inductive Boolean Functions based on Alternating Automata.
    (co-authors: Abdelwaheb Ayari and David Basin)
    In the Proceedings of the 12th International Conference of Computer Aided Verification (CAV 2000).
    Volume 1855 of Lecture Notes in Computer Science, pages 170--185. Springer-Verlag, 2000.
    BibTeX

Chapters in Books:

  1. Complementation of Büchi Automata Using Alternation.
    In Automata, Logics, and Infinite Games (A Guide to Current Research), Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.).
    Volume 2500 of Lecture Notes in Computer Science, pages 61--77, chapter 4. Springer-Verlag, 2002.
    BibTeX

Miscellaneous:

  1. Cases for Including a Reference Monitor to SDN. (Demo)
    (co-authors: Roberto Bifulco, Dimitrios Gkounis, and Ghassan O. Karame)
    In the Proceedings of the 2016 ACM SIGCOMM Conference, 2016.

  2. Fingerprinting Software-defined Networks.
    (co-authors: Roberto Bifulco, Heng Cui, and Ghassan O. Karame)
    In the Proceedings of the 2nd IEEE Workshop on Control, Operation, and Application in SDN Protocols, 2015.
  3. Towards an Access Control Scheme for Accessing Flows in SDN.
    (co-authors: Roberto Bifulco, Heng Cui, and Ghassan O. Karame)
    In the Proceedings of the IEEE Workshop on Security Issues in SDN, 2015.
  4. Access Control for SDN Controllers.
    (co-authors: Roberto Bifulco, Heng Cui, and Ghassan O. Karame)
    In the Proceedings of the 3rd ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking, 2014.
  5. Automatenbasierte Entscheidungsverfahren für Teilsysteme der Arithmetik.
    In Ausgezeichnete Informatikdissertationen 2004, Dorothea Wagner et al. (eds.).
    Lecture Notes in Informatics, pages 65--74, GI-Edition, 2005 (in German).
  6. Automata-based Decision Procedures for Weak Arithmetics.
    PhD Thesis, Institut für Informatik, Albert-Ludwigs-Universität Freiburg, 2004.
    BibTeX
  7. Induktive boolesche Funktionen, endliche Automaten und monadische Logik zweiter Stufe.
    Diplomarbeit, Institut für Informatik, Albert-Ludwigs-Universität Freiburg, 2000 (in German).
    BibTeX

Software:

  1. LIRA: Decision procedures for Presburger arithmetic and the first-order logic over the reals and integers with addition and ordering. LIRA contains a high-performance automata library for deterministic finite automata and weak deterministic Büchi automata.
  2. psl2ba: A translator of the core of the linear-time fragment of the property specification language (PSL) extended with temporal past operators to nondeterministic Büchi automata. The translation is based on two-way alternating automata.
  3. FADecider: A library of algorithms for checking the universality and inclusion of languages given by automata (including visibly pushdown automata) over finite and infinite words.
  4. MONPOLY: A monitoring tool that checks compliance of log files with respect to policies. Policies are specified by formulas in metric first-order temporal logic.

Verantwortlich für den Inhalt dieser Seite ist Felix Klaedtke.