You have come to an old website. Our new URL is Please update your bookmarks!

News and Activities


From 6th to 9th March we organize the "Aachener Informatiktage 2014" in cooperation with the MINT EC association. This Workshop brings former informatic skills to young, interested students.
Find out more at AIT 2014

We thank all participants of our Dagstuhl Seminar ¨Randomized Timed and Hybrid Models for Critical Infrastructures¨ for the great discussions.


We are happy to welcome Gereon Kremer as a PhD student in our group!

Erika Abraham is one of the co-chairs for FORTE'14, a member conference of DisCoTec.
Erika Abraham is a PC member of FORMATS'14.
Erika Abraham will give an invited talk at SFM'14.

Erika Ábrahám is a member of the HSCC'14 program committee.
In cooperation with LuFG I9 we host the pupils university (Schüleruniversität Informatik), which will take place from July 29th until August 2nd.

Our paper "From Statistical Model Checking to Statistical Model Inference: Characterizing the Effect of Process Variations in Analog Circuits" is accepted at ICCAD'13.

Our paper "On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers" was accepted at CAI 2013. We also published a technical report, which is available here.
Our paper "High-level counterexamples for Probabilistic Automata" was accepted at QEST 2013. We also published a technical report including all proofs, which is available here.

We are happy to welcome Stefan Schupp as a PhD student in our group!
Our paper "Lyapunov Function Synthesis using Handelman Representations" is accepted in the invited session of NOLCOS'13.

Our paper "A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition" was accepted at CADE 2013.
Our paper "Flow*: An Analyzer for Non-Linear Hybrid Systems" is accepted at CAV'13.
Our new DFg-funded project HyPro starts, which is done in cooperation with the group of Prof. Kowalewski.
30 high-school students participated at the Aachener Informatiktage.

Our paper "Regular Model Checking Using Solver Technologies and Automata Learning" was accepted at NFM 2013.


Dec 2013: After the evalution it is decided that our group will permanent in form of a W2 professorship.

October 2013: Erika Ábrahám is elected to co-chair TACAS'14.

September 2012: Erika Ábrahám is a member of the TACAS'13 program committee.

August 2012: Our paper "Taylor Model Flowpipe Construction for Non-Linear Hybrid Systems" was accepted at RTSS'12.

July 2012: Our paper "Symbolic Counterexample Generation for Discrete-time Markov Chains" was accepted at FACS'12.

June 2012: Our paper "The COMICS Tool - Computing Minimal Counterexamples for DTMCs" was accepted at ATVA'12.

April 2012: Our paper "SMT-RAT: An SMT-Compliant Non-Linear Real Arithmetic Toolbox" was accepted at SAT'12.

March 2012: Registration is open for the ROCKS Autumn School on Rigorous Dependability Analysis for Stochastic Systems. Registration deadline: July 15, 2012.

March 2012: Joachim Redies' Bachelor Thesis summary is nominated for Best Paper Award at the workshop GI Junge Informatik.

March 2012: 40 high-school students participated at the Aachener Informatiktage and the RWTH MINT Camp 2012.

January 2012: Our paper "Timed CTL Model Checking in Real-Time Maude" was accepted at WRLA'12.

January 2012: Our paper "Some Like It Very Hot: Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude" was accepted at WRLA'12.

January 2012: We released the tool COMICS 1.0, which addresses the computation of small critical subsystems as counterexamples for probabilistic systems. The tool was developed within the CEBug project.


December 2011: Our paper "Hybrid Sequential Function Charts" was accepted at MBMV 2012.

December 2011: Our paper "Minimal Critical Subsystems for Discrete-Time Markov Models" was accepted at TACAS 2012.

December 2011: Our paper "Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties" was accepted at MBMV 2012.

October 2011: Our paper "On Collaboratively Conveying Real-time Systems to Pupils" was accepted at Koli Calling 2011.

4.-9. September, 2011: The "Aachen Concurrency and Dependability Week" will take place, where Nils Jansen and Ulrich Loup participate in the local organization.

August 2011: 40 high-school students had fun at our Schüleruni Informatik (pupils' university in computer science).

June 2011: Our paper "Hierarchical Counterexamples for Discrete-Time Markov Chains" was accepted at ATVA 2011.

June 2011: Best Paper Award at CSSE 2011 for our paper "Formal Modeling and Analysis of Hybrid Systems in Rewriting Logic using Higher-Order Numerical Methods and Discrete-Event Detection".

June 2011: 50 high-school students attended the first lecture of the series "Was ist Informatik?"

June 2011: Our paper "Virtual Substitution for SMT Solving" was accepted at FCT 2011.

May 2011: We published a technical report called "Hierarchical Counterexamples for Discrete-Time Markov Chains".

March 2011: Our paper "Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking" was accepted at FMOODS/FORTE 2011.

March 2011: Our paper "I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra" was accepted at CAI 2011.

March 2011: We organize the "Aachener Informatiktage 2011"  from 10 to 13 March 2011.

February 2011: Our paper "GiNaCRA: A C++ Library for Real Algebraic
Computations" was accepted at NFM 2011.

January 2011: We will offer the proseminar Real-Time Systems in the summer term 2011.




December 2010: Our paper "SMT-based Counterexample Generation for
Markov Chains
" was accepted at MBMV 2011.

December 2010: Our paper "Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems" was accepted at EUROCAST'11.

December 2010: Our paper "Optimisation of Concentrating Solar Thermal Power Plants with Neural Networks" was accepted at ICANNGA'11.

December 2010: Pascal Richter was nominated for student paper award at ICANNGA'11.

October 2010: Our paper "Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems." was accepted at TTSS'10.

October 2010: Our two papers "On the Minimization of Hybrid Automata." and "Rewriting-Logic-Based Formal Modeling and Analysis of Interacting Hybrid Systems." were accepted at NWPT´10.

September 2010: Our paper "Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik" was accepted at DeLFI'10.

August 2010: Ulrich Loup and Nils Jansen participate in the local organisation of CONCUR 2011 and QEST 2011 in Aachen.

July 2010: Our paper "Synthesis of Behavioral Controllers for DES: Increasing Efficiency." was accepted at WODES´10.

June 2010: Die Hellen Köpfe waren bei uns! (Bilder zur Veranstaltung)

  • Die Fachgruppe Informatik richtet dieses Semester erneut das Projekt
    "Helle Köpfe in der Informatik" im Rahmen des "Aachener Modells" aus.
    Dies ist eine Veranstaltung für begabte Grundschüler(innen) aus Stadt
    und Kreis. Dafür wurden Schüler(innen) von den umliegenden Grundschulen
    nominiert und in 8 Terminen an die Informatik herangeführt.
    Wir haben uns mit dem Thema "Rechnen mit Nullen und Einsen"

May 2010: Our paper "DTMC Model Checking by SCC Reduction." was accepted at QEST´10.

April 2010: Our paper "A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra." was accepted at SMT´10.

January 2010: Our paper "Exploiting Different Strategies for the Parallelization of an SMT Solver." was accepted at MBMV'10.

January 2010: In SS10 we offer a proseminar "Real Time Systems".