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). I am also actively developing CAGE, a toolchain which builds on top of AProVE and LoAT to find and prove the absence of denial of service attacks in Java programs. CAGE is joint work of Draper, the University of Innsbruck, and our research group and is developed within the DARPA STAC program.

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

For a rough overview of my research, have a look at this poster and the corresponding extended abstract.

Publications

Show / Hide

Complexity Analysis for Java with AProVE

2017
F. Frohn and J. Giesl
In Proceedings of the 13th International Conference on integrated Formal Methods (iFM '17), Turin, Italy, Lecture Notes in Computer Science 10510, pages 85-101. ©Springer-Verlag

Complexity Analysis for Term Rewriting by Integer Transition Systems

2017
M. Naaf, F. Frohn, M. Brockschmidt, C. Fuhs, and J. Giesl
In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS '17), Brasilia, Brazil, Lecture Notes in Artificial Intelligence 10483, pages 132-150. ©Springer-Verlag

Analyzing Runtime Complexity via Innermost Runtime Complexity

2017
F. Frohn and J. Giesl
In Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '17), Maun, Botswana, EPiC Series in Computing 46, pages 249-268. EasyChair

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, , 59(1):121-163. ©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 10206, pages 350-354. ©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. ©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. ©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. ©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. ©Springer-Verlag

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

Extended Abstracts

Show / Hide

Modular Heap Shape Analysis for Java Programs

2017
F. Frohn and J. Giesl
PhD Symposium at iFM '17 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM '17), Turin, Italy.

Automated Inference of Upper Complexity Bounds for Java Programs

2016
F. Frohn, M. Brockschmidt, and J. Giesl
15th International Workshop on Termination (WST '16), Obergurgl, Austria.

Lower Runtime Bounds for Integer Programs

2016
F. Frohn, M. Naaf, J. Hensel, M. Brockschmidt,and J. Giesl
15th International Workshop on Termination (WST '16), Obergurgl, Austria.

Termination Analysis of Programs with Bitvector Arithmetic by Symbolic Execution

2016
J. Hensel, J. Giesl, F. Frohn, and T. Ströder
15th International Workshop on Termination (WST '16), Obergurgl, Austria.

Awards

Show / Hide

iFM Best Tool Paper Award for "Complexity Analysis for Java with AProVE"

2017

SEFM Recognition Award for "Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution"

2016

Current Activities

Show / Hide

Teaching

Show / Hide

Supervision of 8 Bachelor and 4 Master Theses

WS 13/14 - WS 17/18

Seminar Satisfiability Checking

SS 17

Lecture Formale Systeme, Automaten, Prozesse

SS 16

Seminar Satisfiability Checking

SS 16

Seminar Satisfiability Checking

SS 15

Seminar Satisfiability Checking

SS 14