Peter Schneider-Kamp

Teaching

Current Courses

• Lecture DM820: Advanced Topics in Programming Languages (4th quarter, spring 2012)
• Lecture DM505: Database Design and Programming (3rd quarter, spring 2012)
• Lecture DM503: Programmering B (2nd quarter, fall 2011)
• Lecture DM509: Programming Languages (2nd quarter, fall 2011)
• Lecture DM502: Programmering A (1st quarter, fall 2011)

Past Courses

• Lecture DM503: Programmering B (2nd quarter, fall 2010)
• Lecture DM509: Programming Languages (2nd quarter, fall 2010)
• Lecture DM502: Programmering A (1st quarter, fall 2010)
• Lecture DM509: Programming Languages (2nd quarter, fall 2009)
• Lecture DM526: Introduction to Computer Science (1st & 2nd quarter, fall 2009)
• Lecture DM505: Database Design and Programming (3rd quarter, spring 2009)
• Individual Study Activity DM8XX: Advanced Topics in Programming Languages (4th quarter, spring 2009)
• Vorlesung Programmierung (WS 08/09)
• Seminar Automatische Terminierungsanalyse (WS 08/09)
• Vorlesung Datenstrukturen und Algorithmen (SS 08)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 08)
• Seminar Verifikationsverfahren (SS 08)
• Vorlesung Programmierung (WS 07/08)
• Seminar Automatische Terminierungsanalyse (WS 07/08)
• Vorlesung Functional Programming (SS 07)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 07)
• Seminar Verifikationsverfahren (SS 07)
• Vorlesung Termersetzungssysteme (WS 06/07)
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (WS 06/07)
• Vorlesung Logikprogrammierung (SS 06)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 06)
• Seminar Verifikationsverfahren (SS 06)
• Vorlesung Informatik I - Programmierung (WS 05/06)
• Seminar Automatische Terminierungsanalyse (WS 05/06)
• Vorlesung Functional Programming (SS 05)
• Seminar Verifikationsverfahren (SS 05)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 05)
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (SS 04)
• Proseminar IT-Sicherheitskonzepte und Sicherheit in Java (SS 04)
• Vorlesung Informatik I - Programmierung (WS 03/04)
• Seminar Terminierungsanalyse (WS 03/04)

Research

Automated Software Verification

• Termination of Logic Programs
• Termination of Functional Programs
• Termination of Term Rewriting
• Development of the AProVE Tool
• Termination Analysis of Imperative Programs

Reducing Search Problems to SAT

• Applications in Automated Abstraction and Program Synthesis
• Encoding LPO to SAT
• Encoding RPO to SAT
• Encoding POLO to SAT

Professional Activities

Current Activities & Memberships

• PC-Member of the 14th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2012), Leuven, Belgium, September 2012
• PC-Member of the 12th International Workshop on Termination (WST 2012), Obergurgl, Austria, February 2012
• PC-Member of the 9th International Workshop on the Implementation of Logics (IWIL 2012), Merida, Venezuela, March 2012
• Steering Committee Member of the ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
• Participant in Danish Natural Science Research Council project on Online Algorithms, Bioinformatics, and SAT Solving.
• secretary of the IFIP Working Group 1.6
• Managing Committee substitute member of COST Action IC0901
• Associate Professor at Department of Computer Science & Mathematics at the University of Southern Denmark (SDU)
• member of the Association of Logic Programming
• member of the Association of Automated Reasoning
• founding member of the Python Software Foundation

Past Activities

• General Chair of the 13th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2011), Odense, Denmark, July 2011
• General Chair of the 21st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2011), Odense, Denmark, July 2011
• PC-Chair of the 21st Workshop on Logic-based methods in Programming Environments (WLPE 2011), Lexington, Kentucky, US, July 2011.
• PC-Member of the 3rd International Workshop on Software Engineering for Resilient Systems (SERENE 2011), Geneva, Switzerland, September 2011.
• PC-Member of the 13th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2011), Odense, Denmark, July 2011
• PC-Member of the 21st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2011), Odense, Denmark, July 2011
• PC-Chair of the 11th International Workshop on Termination (WST 2010), Edinburgh, UK, July 2010
• Executive Committee member of ERCIM - the European Research Consortium for Informatics and Mathematics
• Organizer of the Danish Static Analysis Symposium (DANSAS '10), Odense, August 2010
• PC-Member of the 8th International Workshop on the Implementation of Logics (IWIL 2010), Yogyakarta, Indonesia, October 2010
• PC-Member of the 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2010), Hagenberg, Austria, July 2010
• PC-Member of the FLOC 2010 Workshop on Practical Aspects of Automated Reasoning (PAAR 2010), Edinburgh, UK, July 2010
• PC-Member of the Joint Workshop on Implementation of Constraint Logic Programming Systems and Logic-based Methods in Programming Environments (CICLOPS-WLPE 2010), Edinburgh, UK, July 2010
• PC-Member of the 2nd International Workshop on Software Engineering for Resilient Systems (SERENE '10), London, UK, April 2010
• PC-Member of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2009), Coimbra, Portugal, September 2009
• Organizer of the Danish Static Analysis Symposium (DANSAS '09), Odense, August 2009
• PC-Member of the 7th International Workshop on the Implementation of Logics (IWIL 2008), Doha, Qatar, November 2008
• Research and Teaching Assistant at the Research Group Computer Science 2 at RWTH Aachen University, 2003 - 2008
• Editor of the Department Of Computer Science Technical Reports of RWTH Aachen University, 2005 - 2008
• PC-Member of the 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2007), Kongens Lyngby, Denmark, August 2007
• Organizer of TeReSe meeting 2007/2, Aachen, November 2007
• Organizer of TeReSe meeting 2005/2, Aachen, November 2005

Selected Publications

PhD Thesis

• P. Schneider-Kamp
  Static Termination Analysis for Prolog using Term Rewriting and SAT Solving
  December 2008. Available as Technical Report AIB-2008-17, RWTH Aachen University, Germany.

Journals

• C. Fuhs, J. Giesl, M. Parting, P. Schneider-Kamp, and S. Swiderski
  Proving Termination by Dependency Pairs and Inductive Theorem Proving
  Journal of Automated Reasoning, 2011. To appear. © Springer-Verlag
  
• M. Codish, J. Giesl, P. Schneider-Kamp, R. Thiemann
  SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs.
  Journal of Automated Reasoning, 2010. To appear. © Springer-Verlag
• J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann
  Automated Termination Proofs for Haskell by Term Rewriting.
  ACM Transactions on Programming Languages and Systems, 33(2), 2010. To appear. © ACM Publishing
• P. Schneider-Kamp, J. Giesl, T. Ströder, A. Serebrenik, and R. Thiemann
  Automated Termination Analysis for Logic Programs with Cut
  In Proceedings of the 26th International Conference on Logic Programming (ICLP '10), Edinburgh, UK, Theory and Practice of Logic Programming, 10(4-6):365-381, 2010. © Cambridge University Press
  Extended version appeared as Technical Report AIB-2010-10, RWTH Aachen, Germany.
  
• M. T. Nguyen, D. De Schreye, J. Giesl, and P. Schneider-Kamp
  Polytool: Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs
  Theory and Practice of Logic Programming, 2010. To appear. © Cambridge University Press
• P. Schneider-Kamp
  Static Termination Analysis for Prolog Using Term Rewriting and SAT Solving
  KI - Künstliche Intelligenz, 24(1):79-81, 2010. © Springer-Verlag
• P. Schneider-Kamp, J. Giesl, A. Serebrenik, and R. Thiemann
  Automated Termination Proofs for Logic Programs by Term Rewriting
  ACM Transactions on Computational Logic, 11(1): 1-52, 2009. © ACM Publishing
  Preliminary Version
• R. Thiemann, H. Zantema, J. Giesl, and P. Schneider-Kamp
  Adding Constants to String Rewriting
  Applicable Algebra in Engineering, Communication and Computing, 19(1): 27-38, 2008. © Springer-Verlag
  Preliminary Version
• J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
  Mechanizing and Improving Dependency Pairs
  Journal of Automated Reasoning, 37(3): 155-203, 2006. © Springer-Verlag
  Preliminary Version

Conferences

• M. Codish, Y. Fekete, C. Fuhs, and P. Schneider-Kamp
  Optimal Base Encodings for Pseudo-Boolean Constraints
  In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '11), Saarbrücken, Germany, Lecture Notes in Computer Science 6605, 189-204, 2011. © Springer-Verlag
  
• R. Thiemann, C. Sternagel, J. Giesl, and P. Schneider-Kamp
  Loops under Strategies ... Continued
  In Proceedings of the 1st International Workshop on Strategies in Rewriting, Proving, and Programming (IWS '10), Edinburgh, UK, Electronic Proceedings in Theoretical Computer Science 44, 51-65, 2010.
  
• M. Codish, C. Fuhs, J. Giesl, and P. Schneider-Kamp
  Lazy Abstraction for Size-Change Termination
  In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), Yogyakarta, Indonesia, Lecture Notes in Computer Science (ARCoSS) 6397, 217-232, 2010. © Springer-Verlag
  
• T. Ströder, P. Schneider-Kamp, and J. Giesl
  Dependency Triples for Improving Termination Analysis of Logic Programs with Cut
  In Proceedings of the 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '10), Lecture Notes in Computer Science 6564, 184-199, 2011. © Springer-Verlag
  
• C. Fuhs and P. Schneider-Kamp
  Synthesizing Shortest Straight-Line Programs over GF(2) using SAT
  In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT '10), Edinburgh, UK, Lecture Notes in Computer Science 6175, pages 71 - 84, 2010. © Springer-Verlag
  
• P. Schneider-Kamp, J. Giesl, and M. T. Nguyen
  The Dependency Triple Framework for Termination of Logic Programs
  In Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '09), Coimbra, Portugal, Lecture Notes in Computer Science 6037, 37-51, 2010. ©Springer-Verlag
  
• S. Swiderski, M. Parting, J. Giesl, C. Fuhs, and P. Schneider-Kamp
  Termination Analysis by Dependency Pairs and Inductive Theorem Proving
  In Proceedings of the 22nd International Conference on Automated Deduction (CADE '09), Montreal, Canada, Lecture Notes in Artificial Intelligence 5663, 322-338, 2009. ©Springer-Verlag
  
• C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke
  Proving Termination of Integer Term Rewriting
  In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09), Brasilia, Brazil, Lecture Notes in Computer Science 5595, 32-47, 2009. ©Springer-Verlag
  
• B. Alarcon, F. Emmes, C. Fuhs, J. Giesl, R. Gutierrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann
  Improving Context-Sensitive Dependency Pairs
  In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '08), Doha, Qatar, Lecture Notes in Artificial Intelligence 5330, pages 636 - 651, 2008. © Springer-Verlag
  Extended version appeared as Technical Report AIB-2008-13, RWTH Aachen, Germany.
  
• C. Fuhs, R. Navarro, C. Otto, J. Giesl, S. Lucas, and P. Schneider-Kamp
  Search Techniques for Rational Polynomial Orders
  In Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC '08), Birmingham, UK, Lecture Notes in Artificial Intelligence 5144, pages 109-124, 2008. ©Springer-Verlag
  
• C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
  Maximal Termination
  In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA '08), Hagenberg, Austria, Lecture Notes in Computer Science 5117, pages 110-125, 2008. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2008-03, RWTH Aachen, Germany.
  
• R. Thiemann, J. Giesl, P. Schneider-Kamp
  Deciding Innermost Loops
  In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA '08), Hagenberg, Austria, Lecture Notes in Computer Science 5117, pages 366-380, 2008. ©Springer-Verlag
  
• M. T. Nguyen, J. Giesl, P. Schneider-Kamp, and D. De Schreye
  Termination Analysis of Logic Programs based on Dependency Graphs
  In Proceedings of the 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '07), Kongens Lyngby, Denmark, Lecture Notes in Computer Science 4915, pages 8-22, 2008. ©Springer-Verlag
  
• P. Schneider-Kamp, R. Thiemann, E. Annov, M. Codish, and J. Giesl
  Proving Termination using Recursive Path Orders and SAT Solving
  In Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS '07), Liverpool, UK, Lecture Notes in Artificial Intelligence 4720, pages 267-282, 2007. ©Springer-Verlag
  
• J. Giesl, R. Thiemann, S. Swiderski, and P. Schneider-Kamp
  Proving Termination by Bounded Increase
  In Proceedings of the 21st International Conference on Automated Deduction (CADE '07), Bremen, Germany, Lecture Note in Artificial Intelligence 4603, pages 443-459, 2007. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2007-03, RWTH Aachen, Germany.
  
• C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
  SAT Solving for Termination Analysis with Polynomial Interpretations
  In Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT '07), Lisbon, Portugal, Lecture Notes in Computer Science 4501, pages 340-354, 2007. ©Springer-Verlag
  
• M. Codish, P. Schneider-Kamp, V. Lagoon, R. Thiemann, and J. Giesl
  SAT Solving for Argument Filterings
  In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '06), Phnom Penh, Cambodia, Lecture Notes in Artificial Intelligence 4246, pages 30-44, 2006. © Springer-Verlag
  
• J. Giesl, S. Swiderski, P. Schneider-Kamp, and R. Thiemann
  Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
  In Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA-06), Seattle, USA, Lecture Notes in Computer Science 4098, pages 297-312, 2006. ©Springer-Verlag
  
• P. Schneider-Kamp, J. Giesl, A. Serebrenik, and R. Thiemann
  Automated Termination Analysis for Logic Programs by Term Rewriting
  In Proceedings of the 16th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '06), Venice, Italy, Lecture Notes in Computer Science 4407, pages 177-193, 2007. ©Springer-Verlag
  
• J. Giesl, P. Schneider-Kamp, and R. Thiemann
  AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework
  In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR '06), Seattle, USA, Lecture Notes in Artificial Intelligence 4130, pages 281-286, 2006. ©Springer-Verlag
  
• J. Giesl, R. Thiemann, and P. Schneider-Kamp
  Proving and Disproving Termination of Higher-Order Functions
  In Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS '05), Vienna, Austria, Lecture Notes in Artificial Intelligence 3717, pages 216-231, 2005. © Springer-Verlag
  
• J. Giesl, R. Thiemann, and P. Schneider-Kamp
  The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs
  In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '04), Montevideo, Uruguay, Lecture Notes in Artificial Intelligence 3452, pages 301-331, 2005. © Springer-Verlag
  
• R. Thiemann, J. Giesl, and P. Schneider-Kamp
  Improved Modular Termination Proofs Using Dependency Pairs
  In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR '04), Cork, Ireland, Lecture Notes in Artificial Intelligence 3097, pages 75-90, 2004. © Springer-Verlag
  
• J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
  Automated Termination Proofs with AProVE
  In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA '04), Aachen, Germany, Lecture Notes in Computer Science 3091, pages 210-220, 2004. © Springer-Verlag
  
• J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
  Improving Dependency Pairs
  In Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '03), Almaty, Kazakhstan, Lecture Notes in Artificial Intelligence 2850, pages 167-182, 2003. ©Springer-Verlag
  Extended version available as Technical Report AIB-2003-04, RWTH Aachen, Germany.