Stephan Falke

Verification meets Algorithm Engineering

Stephan Falke

Phone: +49-721-608-45955

E-mail: stephan.falke@kit.edu

Home page: http://baldur.iti.kit.edu/~falke/

Research

I am a postdoctoral researcher in the group Verification meets Algorithm Engineering at the Karlsruhe Institute of Technology. I am currently involved in the following research projects:

The Low-Level Bounded Model Checker for C programs LLBMC
The termination prover for C programs KITTeL

I received a Ph.D. from the Department of Computer Science at the University of New Mexico under the supervision of Prof. Deepak Kapur.

As a Masters student I was a member of the AProVE-team in the Research Group Computer Science II at RWTH Aachen University.

Activities

PC-Member of the VERIFY Workshop 2012
PC-Member of the Deduktionstreffen 2011
PC-Member of the Symposium on 75 Years of Turing Machine and Lambda-Calculus (Computing 2011)

Teaching

Publications

List of publications from the DBLP Bibliography Server

Journals

Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke:
Mechanizing and Improving Dependency Pairs
Journal of Automated Reasoning 37(3), pages 155-203, 2006. ©Springer-Verlag
[ Abstract | BibTeX | Preliminary Version (ps.gz) | Preliminary Version (pdf) | Paper on SpringerLink ]

Conferences and Workshops

Stephan Falke, Florian Merz, and Carsten Sinz:
LLBMC: Improved Bounded Model Checking of C Using LLVM (Competition Contribution)
In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '13), Rome, Italy.
Lecture Notes in Computer Science 7795, pages 623-626, 2013. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Stephan Falke, Carsten Sinz, and Florian Merz:
A Theory of Arrays with Set and Copy Operations (Extended Abstract)
In Proceedings of the 10th International Workshop on Satisfiability Modulo Theories (SMT '12), Manchester, UK.
Pages 97-106, 2012.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Florian Merz, Carsten Sinz, and Stephan Falke:
Challenges in Comparing Software Verification Tools for C
In Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE '12), Manchester, UK.
Pages 60-65, 2012.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Stephan Falke and Deepak Kapur:
Rewriting Induction + Linear Arithmetic = Decision Procedure
In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR '12), Manchester, UK.
Lecture Notes in Artificial Intelligence 7364, pages 241-255, 2012. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Carsten Sinz, Florian Merz, and Stephan Falke:
LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation (Competition Contribution)
In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '12), Tallinn, Estonia.
Lecture Notes in Computer Science 7214, pages 542-544, 2012. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Stephan Falke, Deepak Kapur, and Carsten Sinz:
Termination Analysis of Imperative Programs Using Bitvector Arithmetic
In Proceedings of the 4th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '12), Philadelphia, PA, USA.
Lecture Notes in Computer Science 7152, pages 261-277, 2012. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Florian Merz, Stephan Falke, and Carsten Sinz:
LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR
In Proceedings of the 4th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '12), Philadelphia, PA, USA.
Lecture Notes in Computer Science 7152, pages 146-161, 2012. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Stephan Falke, Florian Merz, and Carsten Sinz:
A Theory of C-Style Memory Allocation
In Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT '11), Snowbird, UT, USA.
Technical Report No. UCB/EECS-2011-80, pages 71-80, 2011.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Stephan Falke, Deepak Kapur, and Carsten Sinz:
Termination Analysis of C Programs Using Compiler Intermediate Languages
In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11), Novi Sad, Serbia.
Leibniz International Proceedings in Informatics (LIPIcs) 10, pages 41-50, 2011.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on DROPS ]
Carsten Sinz, Stephan Falke, and Florian Merz:
A Precise Memory Model for Low-Level Bounded Model Checking
In Proceedings of the 5th International Workshop on Systems Software Verification (SSV '10), Vancouver, Canada.
2010.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Stephan Falke and Deepak Kapur:
Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
In Revised Selected Papers from the 18th International Workshop on Functional and (Constraint) Logic Programming (WFLP '09), Brasília, Brazil.
Lecture Notes in Computer Science 5979, pages 44-61, 2010. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Stephan Falke and Deepak Kapur:
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
In Proceedings of the 22nd International Conference on Automated Deduction (CADE '09), Montréal, Canada.
Lecture Notes in Artificial Intelligence 5663, pages 277-293, 2009. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp, and Stephan Falke:
Proving Termination of Integer Term Rewriting
In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09), Brasília, Brazil.
Lecture Notes in Computer Science 5595, pages 32-47, 2009. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Stephan Falke and Deepak Kapur:
Operational Termination of Conditional Rewriting with Built-In Numbers and Semantic Data Structures
In Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS '08), Hagenberg, Austria.
Electronic Notes in Theoretical Computer Science 237, pages 75-90, 2009. ©Elsevier
[ Abstract | BibTeX | Preliminary Version (ps.gz) | Preliminary Version (pdf) | Paper on ScienceDirect ]
Stephan Falke and Deepak Kapur:
Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA '08), Hagenberg, Austria.
Lecture Notes in Computer Science 5117, pages 94-109, 2008. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Stephan Falke and Deepak Kapur:
Dependency Pairs for Rewriting with Non-Free Constructors
In Proceedings of the 21st International Conference on Automated Deduction (CADE '07), Bremen, Germany.
Lecture Notes in Artificial Intelligence 4603, pages 426-442, 2007. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Mahadevan Subramaniam, Deepak Kapur, and Stephan Falke:
Predicting Failures of and Repairing Inductive Proof Attempts
In Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems (Proceedings of the GM R&D Workshop).
Pages 177-192, 2007. ©Springer-Verlag
[ Abstract | BibTeX | Preliminary Version (ps.gz) | Preliminary Version (pdf) | Paper on SpringerLink ]
Stephan Falke and Deepak Kapur:
Inductive Decidability using Implicit Induction
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 45-59, 2006. ©Springer-Verlag
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan 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
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan 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
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]

Academic Publications

Stephan Falke:
Term Rewriting with Built-In Numbers and Collection Data Structures
Ph.D. Dissertation, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2009.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Stephan Falke:
Automated Termination Analysis for Equational Rewriting
Diplomarbeit, Department of Computer Science, Rheinisch-Westfälische Technische Hochschule Aachen, Germany, 2004.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]

Technical Reports

Stephan Falke and Deepak Kapur:
Rewriting Induction + Linear Arithmetic = Decision Procedure
Karlsruhe Report in Informatics 2012-2, Department of Informatics, Karlsruhe Institute of Technology, Germany, 2012.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Stephan Falke, Deepak Kapur, and Carsten Sinz:
Termination Analysis of C Programs Using Compiler Intermediate Languages
Karlsruhe Report in Informatics 2011-6, Department of Informatics, Karlsruhe Institute of Technology, Germany, 2011.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Stephan Falke and Deepak Kapur:
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Technical Report TR-CS-2009-02, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2009.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Stephan Falke and Deepak Kapur:
Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
Technical Report TR-CS-2009-01, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2009.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Erratum (ps.gz) | Erratum (pdf) ]
Stephan Falke and Deepak Kapur:
Proving Termination of Imperative Programs via Term Rewriting
Technical Report TR-CS-2008-03, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2008.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Stephan Falke and Deepak Kapur:
Operational Termination of Conditional Rewriting with Built-In Numbers and Semantic Data Structures
Technical Report TR-CS-2007-22, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2007.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Erratum (ps.gz) | Erratum (pdf) ]
Stephan Falke and Deepak Kapur:
Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
Technical Report TR-CS-2007-21, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2007.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) | Erratum (ps.gz) | Erratum (pdf) ]
Stephan Falke and Deepak Kapur:
Dependency Pairs for Rewriting with Non-Free Constructors
Technical Report TR-CS-2007-07, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2007.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Stephan Falke and Deepak Kapur:
Implicit Induction Methods and Decision Procedures
Technical Report TR-CS-2006-04, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2006.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke:
Mechanizing Dependency Pairs
Technical Report AIB-2003-08, Department of Computer Science, Rheinisch-Westfälische Technische Hochschule Aachen, Germany, 2003.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke:
Improving Dependency Pairs
Technical Report AIB-2003-04, Department of Computer Science, Rheinisch-Westfälische Technische Hochschule Aachen, Germany, 2003.
[ Abstract | BibTeX | Paper (ps.gz) | Paper (pdf) ]

Stephan Falke

Last modified: March 6, 2013