About me

I have been a research assistant and PhD student at Lehr- und Forschungsgebiet Informatik 2 since August 2013. I am one of the main developers of the Automated Program Verification Environment (AProVE) tool. Moreover, the techniques presented in our paper "Lower Runtime Bounds for Integer Programs" are implemented in the freely available Lower bounds Analysis Tool (LoAT). My fields of interest include (but are not limited to):

  • automated termination and complexity analysis of
    • heap-manipulating imperative programs with a focus on Java Bytecode
    • term rewriting systems
    • integer programs
  • abstract interpretation and symbolic evaluation
  • program verification

Publications

Lower Bounds for Runtime Complexity of Term Rewriting

2017
F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder
Journal of Automated Reasoning, to appear. ©Springer-Verlag

AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution)

2017
J. Hensel, F. Emrich, F. Frohn, T. Ströder, and J. Giesl
In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '17), Uppsala, Sweden, Lecture Notes in Computer Science, 2017. To appear. ©Springer-Verlag

Analyzing Program Termination and Complexity Automatically with AProVE

2017
J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann.
Journal of Automated Reasoning, 58(1):3-31, 2017. ©Springer-Verlag

Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic

2017
T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, P. Schneider-Kamp, and C. Aschermann
Journal of Automated Reasoning, 58(1):33-65, 2017. ©Springer-Verlag

Lower Runtime Bounds for Integer Programs

2016
F. Frohn, M. Naaf, J. Hensel, M. Brockschmidt, and J. Giesl
In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR '16), Coimbra, Portugal, Lecture Notes in Artificial Intelligence 9706, pages 550-567, 2016. ©Springer-Verlag

Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution

2016
J. Hensel, J. Giesl, F. Frohn, and T. Ströder
In Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM '16), Vienna, Austria, Lecture Notes in Computer Science 9763, pages 234-252, 2016. ©Springer-Verlag

Winner of the Silver Medal for the second best paper of the conference.

Inferring Lower Bounds for Runtime Complexity

2015
F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder
In Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA '15), Warsaw, Poland, LIPIcs Leibniz International Proceedings in Informatics 36, pages 334-349, 2015. Dagstuhl Publishing

AProVE: Termination and Memory Safety of C Programs (Competition Contribution)

2015
T. Ströder, C. Aschermann, F. Frohn, J. Hensel, and J. Giesl
In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '15), London, UK, Lecture Notes in Computer Science 9035, pages 417-419, 2015. ©Springer-Verlag

Proving Termination and Memory Safety for Programs with Pointer Arithmetic

2014
T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, and P. Schneider-Kamp
In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Vienna, Austria, Lecture Notes in Artificial Intelligence 8562, pages 208-223, 2014. ©Springer-Verlag

Proving Termination of Programs Automatically with AProVE

2014
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
In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Vienna, Austria, Lecture Notes in Artificial Intelligence 8562, pages 184-191, 2014. ©Springer-Verlag

Teaching

Vorlesung Formale Systeme, Automaten, Prozesse

SS 17

Seminar Satisfiability Checking

SS 17

Vorlesung Formale Systeme, Automaten, Prozesse

SS 16

Seminar Satisfiability Checking

SS 16

Seminar Satisfiability Checking

SS 15

Seminar Satisfiability Checking

SS 14