-
Thomas Ströder
|
- Lehr- und Forschungsgebiet Informatik 2
- RWTH Aachen
- 52056 Aachen
- Germany
E-Mail: stroeder@informatik.rwth-aachen.de
- Phone: +49-241/80-21241
- Fax: +49-241/80-22217
- Room: 4209, Ahornstr. 55
|
|
I have been a research assistant and PhD student at
Lehr- und Forschungsgebiet Informatik 2
since March 2010. Moreover, I am one of the main developers of the Automated Program Verification Environment (AProVE) tool.
From March to May 2013, I completed a 12 weeks internship at Microsoft
Research Cambridge under the guidance of Samin
Ishtiaq
and Byron
Cook.
My fields of interest include (but are not limited to):
- Automated Termination Analysis of Imperative Programs based on the Low-Level Virtual Machine (LLVM) Framework
- Automated Verification of Deadlock and Livelock Freedom in Concurrent Programs
- Automated Termination, Complexity, and Determinacy Analysis of Logic Programs
- Abstract Interpretation and Symbolic Evaluation
- Program Verification
- Algorithmic Synthesis
- Artificial Intelligence and Knowledge Representation
|
Organizational Activities
|
-
PC-Member of the 15th
International Workshop on Termination (WST 2016), Obergurgl, Austria,
September 2016
-
Editor of the
RWTH Department Of Computer Science Technical Reports
“Aachener Informatik-Berichte” (AIB)
from December 2011 till November 2015
-
PC-Member of the
4th International Competition on Software Verification (SV-COMP 2015)
held at TACAS, London, UK, April 2015
-
Member of the local organization team of the
Young Researchers'
Conference "Frontiers of Formal Methods" in Aachen, Germany, 2015
-
PC-Chair of the
International Joint Workshop on Implementation
of Constraint and Logic Programming Systems and Logic-based Methods
in Programming Environments 2014 (CICLOPS-WLPE 2014), Vienna,
Austria, July 2014 at the Vienna Summer of Logic (VSL 2014)
-
PC-Member of the 14th
International Workshop on Termination (WST 2014), Vienna, Austria,
July 2014
-
Organizer of the
17th Informal Workshop on Term Rewriting (TeReSe) in Aachen, Germany,
2012
-
Member of the local organization team of the
Girls' Day 2012 in Computer Science at RWTH Aachen in Aachen, Germany,
2012
-
Member of the local organization team of the
Odense
Summer of Logic and Programming in Odense, Denmark, 2011
-
Co-Organizer of the
13th
Informal Workshop on Term Rewriting (TeReSe) in Aachen, Germany, 2010
|
Teaching Activities (Lehr- und Forschungsgebiet Informatik 2)
|
Journals
-
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.
BibTeX
Conferences
-
J. Hensel, J. Giesl, F. Frohn, and T. Ströder
Proving
Termination of Programs with Bitvector Arithmetic by Symbolic
Execution
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. Winner of the Silver
Medal for the second best paper of the conference.
©Springer-Verlag
Extended version appeared as Technical Report AIB-2016-04,
RWTH Aachen, Germany.
BibTeX
-
F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder
Inferring
Lower Bounds for Runtime Complexity
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.
Extended version appeared as Technical Report AIB-2015-05,
RWTH Aachen, Germany.
BibTeX
-
T. Ströder, C. Aschermann, F. Frohn, J. Hensel, J. Giesl
AProVE: Termination and Memory Safety of C Programs
- (Competition Contribution)
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
BibTeX
-
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 Artificial
Intelligence 8562, pages 208-223, 2014.
©Springer-Verlag
Extended version appeared as Technical Report AIB-2014-05,
RWTH Aachen, Germany.
BibTeX
-
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 Artificial
Intelligence 8562, pages 184-191, 2014.
©Springer-Verlag
BibTeX
-
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.
Slides of a related talk by J. Giesl.
BibTeX
-
M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl
Automated Detection of
Non-Termination and
NullPointerExceptions for Java
Bytecode
In Proceedings of the 2nd International Conference on Formal
Verification of Object-Oriented Software (FoVeOOS '11), Turin,
Italy, Lecture Notes in Computer Science 7421, pages 123-141, 2012.
©Springer-Verlag
Extended
version appeared as Technical Report AIB-2011-19, RWTH Aachen,
Germany.
An
experimental evaluation of the presented techniques is available.
Slides
for the presentation by M. Brockschmidt at FoVeOOS '11 (won best
paper and presentation award)
BibTeX
-
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,
2011, Lecture Notes in Computer Science 7225, pages 237-252, 2012.
©Springer-Verlag
Extended version appeared as Technical Report AIB-2011-08,
RWTH Aachen, Germany.
BibTeX
-
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),
Hagenberg, Austria, Lecture Notes in Computer Science 6564,
pages 184-199, 2011.
©Springer-Verlag
Extended version appeared as Technical Report AIB-2010-12,
RWTH Aachen, Germany.
BibTeX
-
T. Ströder and M. Pagnucco
Realising
Deterministic Behavior from Multiple Non-Deterministic Behaviors
In Proceedings of the 21st International Joint Conference on
Artificial Intelligence (IJCAI '09),
Pasadena, California, USA, pages 936-941, 2009.
©Morgan Kaufmann Publishers Inc.
BibTeX
Proceedings
Informal Publications
-
F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder
Inferring Lower Bounds for Runtime Complexity
RWTH Aachen University Technical Report (Aachener Informatik Berichte)
AIB-2015-05, Aachen, Germany, 2015.
BibTeX
-
T. Ströder
Transformational Termination Analysis of Programs with Pointer
Arithmetic
In Proceedings of the Young Researchers' Conference "Frontiers of
Formal Methods" (FFM '15), Aachen, Germany, 2015.
BibTeX
-
B. Cook, S. Magill, M. Parkinson, and T. Ströder
Reducing Deadlock and Livelock Freedom to Termination
In Proceedings of the 14th International Workshop on Termination
(WST '14), Vienna, Austria, 2014.
BibTeX
-
T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel,
and P. Schneider-Kamp
Automated Termination Analysis for Programs with Pointer
Arithmetic
RWTH Aachen University Technical Report (Aachener Informatik Berichte)
AIB-2014-05, Aachen, Germany, 2014.
BibTeX
-
T. Ströder, F. Emmes, P. Schneider-Kamp, and J. Giesl
Automated Runtime Complexity Analysis for Prolog by Term Rewriting
In Proceedings of the 12th International Workshop on Termination
(WST '12), Obergurgl, Austria, 2012.
BibTeX
-
M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl
Proving Non-Termination for Java Bytecode
In Proceedings of the 12th International Workshop on Termination
(WST '12), Obergurgl, Austria, 2012.
BibTeX
-
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
RWTH Aachen University Technical Report (Aachener Informatik Berichte)
AIB-2012-12, Aachen, Germany, 2012.
BibTeX
-
T. Ströder, F. Emmes, J. Giesl, P. Schneider-Kamp, and C. Fuhs
Automated Complexity Analysis for Prolog by Term Rewriting
RWTH Aachen University Technical Report (Aachener Informatik Berichte)
AIB-2012-05, Aachen, Germany, 2012.
BibTeX
-
T. Ströder
Graph-based Methods for Analysis and Synthesis of Programs
In Proceedings of the Joint Workshop of the German Research Training
Groups in Computer Science, Dagstuhl, Germany, 2011.
©GITO mbH Verlag
BibTeX
-
M. Brockschmidt, T. Ströder, C. Otto, J. Giesl
Automated Detection of Non-Termination and NullPointerExceptions for Java
Bytecode
RWTH Aachen University Technical Report (Aachener Informatik Berichte)
AIB-2011-19, Aachen, Germany, 2011.
BibTeX
-
T. Ströder, F. Emmes, P. Schneider-Kamp, J. Giesl, C. Fuhs
A Linear Operational Semantics for Termination and Complexity Analysis of
ISO Prolog
RWTH Aachen University Technical Report (Aachener Informatik Berichte)
AIB-2011-08, Aachen, Germany, 2011.
BibTeX
-
T. Ströder, J. Giesl and P. Schneider-Kamp
Termination Analysis of Logic Programs with
Cut Using Dependency Triples
In Proceedings of the 11th International Workshop on Termination
(WST '10), Edinburgh, UK, 2010.
BibTeX
-
T. Ströder, P. Schneider-Kamp, J. Giesl
Dependency Triples for Improving Termination Analysis of Logic Programs
with Cut
RWTH Aachen University Technical Report (Aachener Informatik Berichte)
AIB-2010-12, Aachen, Germany, 2010.
BibTeX
-
P. Schneider-Kamp, J. Giesl, T. Ströder, A. Serebrenik,
R. Thiemann
Automated Termination Analysis for Logic Programs with Cut
RWTH Aachen University Technical Report (Aachener Informatik Berichte)
AIB-2010-10, Aachen, Germany, 2010.
BibTeX
