Felix Klaedtke

Address:	ETH Zurich Computer Science Department Universitätstr. 6 CNB F 107.1 CH-8092 Zurich, Switzerland
Phone:	+41 (0)44 63 27639
Email:	felixkl_X_inf.ethz.ch or
	felix.klaedtke_X_inf.ethz.ch (where _X_ actually means @)

Journal Articles:

1. 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.
   Abstract BibTeX DOI PDF (preprint)
2. Ehrenfeucht-Fraisse Goes Automatic for Real Addition.
   Information and Computation, Volume 208, Issue 11, 2010.
   Abstract BibTeX DOI PDF (preprint)
3. On Regular Temporal Logics with Past.
   (co-authors: Christian Dax and Martin Lange)
   Acta Informatica, Volume 47, Issue 4, 2010.
   Abstract BibTeX DOI PDF (preprint)
4. 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, Numbers 1-3, 2008.
   Abstract BibTeX DOI PDF (preprint)
5. Bounds on the Automata Size for Presburger Arithmetic.
   ACM Transactions on Computational Logic, Volume 9, Issue 2, 2008.
   Abstract BibTeX DOI PDF (preprint)
   
6. Decision Procedures for Inductive Boolean Functions Based on Alternating Automata.
   (co-authors: Abdelwaheb Ayari and David Basin)
   Theoretical Computer Science, Volume 300, Numbers 1-3, 2003.
   Abstract BibTeX DOI gzip'ed PostScript (preprint)

Conference Papers:

1. 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.
   Abstract BibTeX PDF
   The orginal publication will be available at www.springerlink.com.
2. 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 orginal publication will be available at www.springerlink.com.
3. 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.
   Abstract BibTeX PDF PDF (full version)
   The orginal publication will be available at www.springerlink.com.
4. 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.
   Abstract BibTeX PDF PDF (full version)
5. 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.
   Abstract BibTeX PDF PDF (full version)
   The orginal publication is available at www.springerlink.com.
6. 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.
   Abstract BibTeX PDF
7. 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.
   Abstract BibTeX PDF
8. 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.
   Abstract BibTeX PDF
9. 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.
   Abstract BibTeX PDF PDF (full version)
10. 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.
    Abstract BibTeX PDF PDF (full version)
11. Alternation Elimination by Complementation.
    (co-author: Christian Dax)
    In the Proceedings of the 15th International Conference on Logic for Programming, Aritificial Intelligence and Reasoning (LPAR 2008).
    Volume 5330 of Lecture Notes in Computer Science, pages 214--229, Springer-Verlag, 2008.
    Abstract BibTeX PDF PDF (full version)
12. 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.
    Abstract BibTeX PDF PDF (full version)
13. 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.
    Abstract BibTeX PDF
14. 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 web page
15. 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.
    Abstract BibTeX gzip'ed PostScript PDF
16. 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.
    Abstract BibTeX gzip'ed PostScript (with proof details)
17. 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.
    Abstract BibTeX gzip'ed PostScript
18. 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.
    Abstract BibTeX
    An extended version of the paper containing all proof details is available here.
19. 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.
    Abstract BibTeX
    
20. 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.
    Abstract BibTeX
    
21. 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.
    Abstract 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
   

Technical Reports:

1. Don't Care Words with an Application to the Automata-based Approach for Real Addition
   (co-author: Jochen Eisinger)
   Technical Report No. 223 of the Institute of Computer Science at Freiburg University, 2006.
2. Optimizing Bounded Model Checking for Linear Hybrid Systems - Theory and Experimental Results
   (co-authors: Erika Abraham, Bernd Becker, and Martin Steffen)
   Technical Report No. 214 of the Institute of Computer Science at Freiburg University, 2004.
3. On the Automata Size for Presburger Arithmetic.
   Technical Report No. 186 of the Institute of Computer Science at Freiburg University, 2003.
   
4. Parikh Automata and Monadic Second-Order Logics with Linear Cardinality Constraints.
   (co-author: Harald Ruess)
   Technical Report No. 177 of the Institute of Computer Science at Freiburg University, 2002.
   A revised version (with some corrections and extensions) can be found here.
5. WS1S with Cardinality Constraints.
   (co-author: Harald Ruess)
   CSL Technical Report SRI-CSL-04-01, SRI International, 2001
   

Miscellaneous:

1. 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).
2. Automata-based Decision Procedures for Weak Arithmetics.
   PhD Thesis, Institut für Informatik, Albert-Ludwigs-Universität Freiburg, 2004.
   BibTeX
   
3. Induktive boolesche Funktionen, endliche Automaten und monadische Logik zweiter Stufe.
   Diplomarbeit, Institut für Informatik, Albert-Ludwigs-Universität Freiburg, 2000 (in German).
   BibTeX
   

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. 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.

1. Runtime Monitoring of Timed Software Systems
2. Symbolic Implementation of PastPSL
3. PastPSL for the SPIN Model Checker

1. FS 10: Co-Lecturer of the course Formal System Development.
2. FS 10: Lecturer of the course Model Checking.
3. FS 09: Lecturer of the course Model Checking.
4. SS 08: Co-Lecturer of the course Formal Methods and Functional Programing.
5. WS 06/07: Co-lecturer of the course Computer-supported Modeling and Reasoning.
6. WS 05/06: Lecturer of the course Decision Procedures for Logical Theories.
7. WS 02/03: Co-lecturer of the course Automata-Based System Analysis.
8. 5-16 August 2002: Co-lecturer of the ESSLLI course Monadic Second-Order Logics: Theory and Practice.
9. SS 02: Co-lecturer of the course Automata-Based System Analysis.

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