profile picture

Florian Frohn

Computer Scientist

Education

Dr. rer. nat. in Computer Science

RWTH Aachen University
2013 - 2018

MSc in Computer Science

RWTH Aachen University
2011 - 2013

BSc in Computer Science

Fernuniversität Hagen
2007 - 2011
part-time until 2009

Interests

About me

I am a tenured lecturer ("Lehrkraft für besondere Aufgaben") in the research group Programming Languages and Verification at RWTH Aachen. I am/have been contributing to several software projects:

  • Our techniques to prove lower runtime-bounds and non-termination of integer programs as well as (un)satisfiability of CHCs are implemented in the freely available Loop Acceleration Tool (LoAT).
  • I am one of the main developers of the Automated Program Verification Environment (AProVE).
  • Our techniques to solve SMT problems with integer exponentiation are implemented in the freely available tool SwInE
  • I was one of the main developers of Astrée from 05/2020 to 03/2022.
  • I contributed to CAGE, a toolchain which uses 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 was developed within the DARPA STAC program.

My fields of interest include (but are not limited to):

  • satisfiability of CHCs
  • SMT
  • automated safety, termination, and complexity analysis of
    • imperative programs
    • term rewriting systems
    • transition systems
  • abstract interpretation
  • program verification

Publications

Show / Hide

Integrating Loop Acceleration into Bounded Model Checking

2024
F. Frohn and J. Giesl
In Proceedings of the 26th International Symposium on Formal Methods (FM '24), Milan, Italy, to appear

Satisfiability Modulo Exponential Integer Arithmetic

2024
F. Frohn and J. Giesl
In Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR '24), Nancy, France, Lecture Notes in Artificial Intelligence 14739, pages 344-365. ©Springer-Verlag

From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting

2024
J.-C. Kassing, F. Frohn, and J. Giesl
In Proceedings of the 27th Conference on Foundations of Software Science and Computation Structures (FoSSaCS '24), Luxembourg City, Luxembourg, Lecture Notes in Computer Science 14575, pages 206-228. ©Springer-Verlag

Proving Non-Termination by Acceleration Driven Clause Learning with LoAT

2023
F. Frohn and J. Giesl
In Proceedings of the 29th Conference on Automated Deduction (CADE '23), Rome, Italy, Lecture Notes in Computer Science 14132, pages 220-233. ©Springer-Verlag

ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses

2023
F. Frohn and J. Giesl
In Proceedings of the 30th Static Analysis Symposium (SAS '23), Cascais, Portugal, Lecture Notes in Computer Science 14284, pages 259-285. ©Springer-Verlag

Termination of Triangular Polynomial Loops

2023
M. Hark, F. Frohn, and J. Giesl
Formal Methods in System Design. ©Springer-Verlag

Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)

2022
F. Frohn and J. Giesl
In Proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR '22), Haifa, Israel, Lecture Notes in Artificial Intelligence 13385, pages 712-722. ©Springer-Verlag

A Calculus for Modular Loop Acceleration and Non-Termination Proofs

2022
F. Frohn and C. Fuhs
International Journal on Software Tools for Technology Transfer, 24(5) ©Springer-Verlag

Polynomial Loops: Beyond Termination

2020
M. Hark, F. Frohn, and J. Giesl
In Proceedings of the 23rd International Conference on logic for programming, artificial intelligence and reasoning (LPAR '20). EPiC Series in Computing 73, pages 279-297. EasyChair

A Calculus for Modular Loop Acceleration

2020
F. Frohn
In Proceedings of the 26rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '20). Lecture Notes in Computer Science 12078, pages 58-76. ©Springer-Verlag

Termination for Polynomial Loops

2020
F. Frohn, M. Hark, and J. Giesl
In Proceedings of the 27th Static Analysis Symposium (SAS '20), Chicago, IL, USA, Lecture Notes in Computer Science, to appear. ©Springer-Verlag

Inferring Lower Runtime Bounds for Integer Programs

2020
F. Frohn, M. Naaf, M. Brockschmidt, and J. Giesl
ACM Transactions on Programming Languages and Systems, 42(3).

Proving Non-Termination via Loop Acceleration

2019
F. Frohn and J. Giesl
In Proceedings of the 19th International Conference on Formal Methods in Computer-Aided Design (FMCAD '19), San Jose, CA, USA. IEEE Press, pages 221-230.

Termination of Triangular Integer Loops is Decidable

2019
F. Frohn and J. Giesl
In Proceedings of the 31st International Conference on Computer Aided Verification (CAV '19), New York, NY, USA, Lecture Notes in Computer Science 11562, pages 426-444. ©Springer-Verlag

Automated Complexity Analysis of Rewrite Systems

2018
F. Frohn
PhD thesis, RWTH Aachen

Constant Runtime Complexity of Term Rewriting is Semi-Decidable

2018
F. Frohn and J. Giesl
Information Processing Letters, 139:18-23, 2018. ©Elsevier

Termination and Complexity Analysis for Programs with Bitvector Arithmetic by Symbolic Execution

2018
J. Hensel, J. Giesl, F. Frohn, T. Ströder
Journal of Logical and Algebraic Methods in Programming, 97:105-130, 2018. ©Elsevier

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

Proving Non-Termination by Acceleration Driven Clause Learning

2023
F. Frohn and J. Giesl
19th International Workshop on Termination (WST '23), Obergurgl, Austria.

A Calculus for Modular Non-Termination Proofs by Loop Acceleration

2022
F. Frohn and C. Fuhs
18th International Workshop on Termination (WST '22), Haifa, Israel.

Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity

2022
M. Hark, F. Frohn, and J. Giesl
18th International Workshop on Termination (WST '22), Haifa, Israel.

Polynomial Loops: Termination and Beyond

2021
F. Frohn, M. Hark, and J. Giesl
17th International Workshop on Termination (WST '21), virtual event.

Complexity Analysis for Bitvector Programs

2018
J. Hensel, F. Frohn, and J. Giesl
16th International Workshop on Termination (WST '18), Oxford, UK.

AProVE at the Termination Competition 2018

2018
M. Brockschmidt, S. Dollase, F. Emrich, F. Frohn, C. Fuhs, J. Giesl, M. Hark, J. Hensel, D. Korzeniewski, M. Naaf, abd T. Ströder
16th International Workshop on Termination (WST '18), Oxford, UK.

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.

Automatic Complexity Analysis of Programs

2017
F. Frohn and J. Giesl
9th International School on Rewriting, Eindhoven, The Netherlands.

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

EASST Award for the best ETAPS paper related to the systematic and rigorous engineering of software and systems for "A Calculus for Modular Loop Acceleration"

2020

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

2017

ISR Best Poster Award for this poster

2017

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

2016

CADE Woody Bledsoe Travel Award

2016

Current Activities

Show / Hide

Organizer and head of the Steering Committee of the Termination and Complexity Competition (termCOMP)

since 2023

PC-Member of the 11th Workshop on Horn Clauses for Verification and Synthesis (HCVS '24)
Luxembourg City, Luxembourg

2024

PC-Member of the 19th International Workshop on Termination (WST '23)
Obergurgl, Austria

2023

PC-Member of the 18th International Workshop on Termination (WST '22)
Haifa, Israel

2022

PC-Member of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '20)
Alicante, Spain

2020

PC-Member of the 17th International Workshop on Termination (WST '20)
Paris, France
Canceled due to COVID-19

2020

Member of the Steering Committee of the Termination and Complexity Competition (TermComp)

since 2020

Participant of the Dagstuhl-seminar Deduction Beyond Satisfiability
Dagstuhl, Germany

2019

PC-Member of the 9th Workshop on Developments in Implicit Computational Complexity (DICE '18)
Thessaloniki, Greece

2018

Teaching

Show / Hide

Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts)

SS 24

Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts)

SS 23

Verifikationsverfahren (Verification Techniques)

WS 22/23

Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts)

SS 22

Seminar Satisfiability Checking

SS 22

Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts)

SS 17

Seminar Satisfiability Checking

SS 17

Lecture Programmierung (Programming Concepts)

WS 16/17

Seminar Verifikationsverfahren (Verification Techniques)

WS 16/17

Lecture Formale Systeme, Automaten, Prozesse

SS 16

Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts)

SS 16

Seminar Satisfiability Checking

SS 16

Lecture Termersetzungssysteme (Term Rewriting Systems)

WS 15/16

Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (Advanced Topics in Term Rewriting)

WS 15/16

Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts)

WS 15/16

Lecture Formale Systeme, Automaten, Prozesse

SS 15

Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts)

SS 15

Seminar Satisfiability Checking

SS 15

Lecture Programmierung (Programming Concepts)

WS 14/15

Seminar Verifikationsverfahren (Verification Techniques)

WS 14/15

Lecture Funktionale Programmierung (Functional Programming)

SS 14

Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts)

SS 14

Seminar Satisfiability Checking

SS 14

Lecture Programmierung (Programming Concepts)

WS 13/14