Teaching

Current Courses

Lecture DM850: Satisfiability (2nd semester, spring 2016)

Past Courses

Lecture DM550: Introduction to Programming (1st semester, fall 2015)
Lecture DM536: Introduction to Programming (1st quarter, fall 2015)
Lecture DM519: Concurrent Programming (3rd quarter, spring 2015)
Lecture DM550: Introduction to Programming (1st semester, fall 2014)
Lecture DM536: Introduction to Programming (1st quarter, fall 2014)
Lecture DM519: Concurrent Programming (3rd quarter, spring 2014)
Lecture DM537: Object-oriented Programming (2nd quarter, fall 2013)
Lecture DM536: Introduction to Programming (1st quarter, fall 2013)
Lecture DM519: Concurrent Programming (3rd quarter, spring 2013)
Lecture DM537: Object-oriented Programming (2nd quarter, fall 2012)
Lecture DM509: Programming Languages (1st quarter, fall 2012)
Lecture DM536: Introduction to Programming (1st quarter, fall 2012)
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)
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
Termination of Imperative Programs

Development of the AProVE Tool

Reducing Search Problems to SAT

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

Sorting Networks

Minimal Size Sorting Networks
Minimal Depth Sorting Networks
Efficient Sorting based on Sorting Networks

Professional Activities

Current Activities & Memberships

PC-Member of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, UK, September 2016
PC-Member of the 7th International Conference on Ambient Systems, Networks and Technologies (ANT 2016), Madrid, Spain, May 2016.
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.
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 for Automated Reasoning
founding member of the Python Software Foundation

Past Activities

secretary of the IFIP Working Group 1.6
Managing Committee substitute member of COST Action IC0901
PC-Member of the 11th International Workshop on the Implementation of Logics (IWIL 2015), Suva, Fiji, 2015
PC-Member of the 6th International Conference on Ambient Systems, Networks and Technologies (ANT 2015), London, UK, June 2015.
PC-Member of the 7th International Workshop on Software Engineering for Resilient Systems (SERENE 2015), Paris, France, September 2015.
PC-Member of the 6th International Workshop on Software Engineering for Resilient Systems (SERENE 2014), Budapest, Hungary, October 2014.
PC-Member of the 14th International Workshop on Termination (WST 2014), Vienna, Austria, July 2014
PC-Member of the 5th International Conference on Ambient Systems, Networks and Technologies (ANT 2014), Hasselt, Belgium, June 2014.
PC-Member of the 2nd Joint Workshop on Implementation of Constraint Logic Programming Systems and Logic-based Methods in Programming Environments (CICLOPS-WLPE 2014), Vienna, Austria, July 2014.
PC-Member of the 5th International Workshop on Software Engineering for Resilient Systems (SERENE 2013), Kiev, Ukraine, October 2013.
PC-Member of the 22nd International Workshop on Functional and (Constraint) Logic Programming (WFLP 2013), Kiel, Germany, September 2013.
PC-Member of the 23rd Workshop on Logic-based methods in Programming Environments (WLPE 2013), Madrid, Spain, August 2013.
PC-Member of the 13th International Workshop on Termination (WST 2013), Bertinoro, Italy, August 2013
PC-Member of the 11th International Symposium on Functional and Logic Programming (FLOPS 2012), Kobe, Japan, May 2012
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 22nd Workshop on Logic-based methods in Programming Environments (WLPE 2012), Budapest, Hungary, September 2012.
PC-Member of the 4th International Workshop on Software Engineering for Resilient Systems (SERENE 2012), Pisa, Italy, 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
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, 47(2):133-160, 2011. © 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, 49(1):53-93, 2012. © 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), 2011. © 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, 11(1):33-63, 2011. © 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

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

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

Conferences

F. Hargreaves, D. Merkle, P. Schneider-Kamp
Group Communication Patterns for High Performance Computing in Scala
In Proceedings of the 3rd ACM SIGPLAN Workshop on Functional High-Performance Computing (FHPC '14), Gothenburg, Sweden, 2014. ©ACM Press. To appear.

T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, and P. Schneider-Kamp
Proving Termination and Memory Safety for Programs with Pointer Arithmetic
In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Vienna, Austria, Lecture Notes in Computer Science, 2014. To appear. © Springer-Verlag
Extended version appeared as Technical Report AIB-2014-05, RWTH Aachen, Germany.

J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann
Proving Termination of Programs Automatically with AProVE
In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Vienna, Austria, Lecture Notes in Computer Science, 2014. To appear. © Springer-Verlag

J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs
Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs
In Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12), Leuven, Belgium, pages 1-12, 2012. ©ACM Press.
Extended version appeared as Technical Report AIB-2012-12, RWTH Aachen, Germany.

T. Ströder, F. Emmes, P. Schneider-Kamp, J. Giesl, and C. Fuhs
A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog
In Proceedings of the 21st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '11), Odense, Denmark, Lecture Notes in Computer Science. To appear. ©Springer-Verlag
Extended version appeared as Technical Report AIB-2011-08, RWTH Aachen, Germany.

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.

Design by 1234.info | Modified by Peter Schneider-Kamp | CSS 2.0