Past Events

Events in 2015

  • Markus Rabe: Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains

    16th Jan 2015 10:00:am
    Venue: E3 Room 2.22

    Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains   Abstract: We present a novel technique to analyze the bounded reachability probability problem for large Markov chains. The essential idea is to incrementally search for sets of paths that lead to the goal region and to choose the sets in a way that...

  • Presentation of Martin Zimmermann and Felix Klein

    22nd Jan 2015 2:00:pm
    Venue:

    Speaker: Martin Zimmermann, Universität des Saarlandes Title: The Complexity of Counting Models of Linear-time Temporal Logic Abstract: We determine the complexity of counting models of bounded size of specifications expressed in Linear-time Temporal Logic. Counting word models is #P-complete, if the bound is given in unary, and as hard as counting accepting runs of non-deterministic...

  • Presentation Srivathsan Baluguru

    2nd Feb 2015 4:00:pm
    Venue: Room 9220

    Fast detection of cycles in timed automata Abstract: We will present an algorithm to detect if a cycle in a timed automaton can be iterated infinitely often. Existing solutions in tools have a complexity which is exponential in the number of clocks. Our method is polynomial. This method can be incorporated in algorithms for verifying...

  • Gedenkkolloquium zu Ehren von Prof. Berthold Vöcking

    5th Feb 2015 12:00:pm
    Venue:

    Die Fachgruppe Informatik gedenkt mit einem zweitägigen Kolloquium am 5. und 6. Februar 2015 ihrem leider viel zu früh verstorbenen Freund und Kollegen Berthold Vöcking und lädt dazu herzlich ein. Am Donnerstag ab 12 Uhr beginnt das Kolloquium mit einem Empfang vor dem AH 5. Ab ca. 13 Uhr beginnen die Vorträge seiner Freunde, Kollegen...

  • Young Researchers Conference

    24th Feb 2015 7:00:pm
    Venue:

    19:00 – 21:30 Welcome (with drinks and snacks) at “SuperC”, RWTH Aachen (6th Floor)

  • Young Researchers Conference

    25th Feb 2015 9:00:am
    Venue:

    9:00 – 9:15 Welcome 9:15 – 10:15 Moshe Vardi: The Rise and fall of Linear Temporal Logic Coffee Break 10:30 – 11:30 Shiguang Feng : Path-Checking for MTL and TPTL over Data Words Claudia Carapelle : Satisfiability of ECTL* with constraints Sascha Wunderlich : Weight Monitoring with Linear Temporal Logic Normann Decker : On an Extension of Freeze LTL...

  • Young Researchers Conference

    26th Feb 2015 9:00:pm
    Venue:

    9:00 – 10:00 Jean-Francois Raskin: Variations on the stochastic shortest path problem Coffee Break 10:20 – 11:20 Vitaly Perevoshchikov : Decomposition of Weighted Timed Automata Parvaneh Babari : A Nivat Theorem for Weighted Picture Automata and Weighted MSO Logics Mohamed Abdelaal : Fuzzy Compression Refinement via Curvature Tracking Saifullah Khan : Traffic Data Dissemination in Realistic Urban VANETs Environment Andreas...

  • Young Researchers Conference

    27th Feb 2015 9:00:am
    Venue:

    9:00 – 10:00 Eric Bodden: SPLlift: statically analyzing software product lines in minutes instead of years Coffee Break 10:20 – 11:20 Bogdan Mihaila : Synthesizing Predicates from Abstract Domain Losses Suvam Mukherjee : Efficient Shape Analysis of Multithreaded Programs Mitra Tabaei Befrouei : Abstraction and Mining of Traces to Explain Concurrency Bugs Christian Müller : An Analysis of Universal Information...

  • Vortrag: Die 2 Seiten der Gläsernen Decke

    3rd Mar 2015 5:00:pm
    Venue:

    „Die 2 Seiten der Gläsernen Decke“,  gehalten von Marion Knaths am 03.03 um 17h im SuperC, Generali Saal – Templergraben 55, 6. Etage Frauen in Spitzenpositionen sind immer noch eine Ausnahme. Oftmals wird die berühmte „Gläserne Decke“ als Ursache dafür zitiert. Oben in der Regel die machthabenden Männer, unten in der Regel die aufstrebenden Frauen....

  • Kinoabend: The Imitation Game

    4th Mar 2015 6:00:pm
    Venue:

    Wer hat Lust auf Kino? Alle sind herzlich eingeladen mitzukommen! Wir – das ist eine Initiative aus REGINA e.V. und der GI-Regionalgruppe Aachen (RIA) – haben einen Saal im Apollo-Kino reserviert und gezeigt wird: The Imitation Game Am 4. März 2015 um 18 Uhr Im Apollo Kino&Bar, Pontstraße 141-149, 52062 Aachen Der Film von Morten Tyldum...

  • Presentation Arend Rensink

    9th Mar 2015 3:30:pm
    Venue: Room 4017 , Seminarraum i1

    If-Next-Also-Else: Controlling Graph Transformation Abstract: Graph transformation is a declarative, rule-based formalism. However, when using it in practice, it is convenient to schedule rules explicitly, and not just rely on their own application conditions, even though such scheduling adds an imperative flavour. This can be catered for by adding a layer of *control* on top...

  • Seminar: Professor Chris Myers, University of Utah, USA

    17th Mar 2015 2:00:pm
    Venue: Room 4017 , Seminarraum i1

    An Integrated Verification Architecture Abstract: Research in formal verification is hampered by a lack of an integrated verification architecture. Each verification tool in development typically uses its own language for models and properties. This fact means that when a designer wants to verify their system using multiple verification tools, it often requires a time-consuming and...

  • Presentation: Prof. Sriram Sankaranarayanan

    24th Mar 2015 11:00:am
    Venue: Room 9222, E3

    Switched Region Stabilization of Polynomial Dynamical Systems Abstract: We consider the problem of automatically synthesizing region stabilizing controllers for polynomial dynamical systems. The goal of our synthesis is to produce switching controllers that can switch between finitely many modes to ensure that the resulting closed loop dynamics are guaranteed to reach a given small target...

  • Presentation: Prof. Luca Bortolussie (Trieste, Italy)

    25th Mar 2015 2:00:pm
    Venue: Room 5052

    Machine Learning meets Formal Verification Abstract: We will discuss novel applications of state-of-the-art Machine Learning statistical tools to deal with uncertainty in Continuous Time Markov Chains, combining them with classic tools from formal methods, mainly Model Checking. Uncertain CTMC are Markov Chains whose rates depend on some fixed parameter, whose precise value is unknown, but...

  • Presentation: Roberta Lanciani

    25th Mar 2015 4:00:pm
    Venue:

    Stochastic Approximations and Verifications In this talk, we discuss the use of stochastic approximations to validate properties of Markov population models. This type of Markovian models are used to describe the evolution of large systems of interacting entities, and their verification, using standard stochastic model checking techniques, is ampered by the large number of possible...

  • Presentation: Nils Jansen

    26th Mar 2015 10:00:am
    Venue: Room 9222, E3

    Counterexamples in Probabilistic Verification The topic of this thesis is roughly to be classified into the formal verification of probabilistic systems. In particular, the generation of counterexamples for discrete-time Markov Models is investigated. A counterexample for discrete-time Markov Chains (DTMCs) is classically defined as a (finite) set of paths. In this work, this set of...

  • Prof. Lijun Zhang: Polynomial Quantitative Loop Invariants by Lagrange Interpolation

    22nd Apr 2015 10:00:am
    Venue:

    Polynomial Quantitative Loop Invariants by Lagrange Interpolation   Abstract: We apply multivariate Lagrange interpolation to synthesizing polynomial quantitative loop invariants for probabilistic programs. Lagrange interpolation allows to find better constraints for unknown loop invariants. Random sampling furthermore generates constraints to pin- point quantitative invariants. We evaluate our technique by several case studies with polynomial quantitative...

  • Deni Raco: Umsetzung der formalen Entwicklungsmethodik FOCUS in dem Theorembeweiser Isabelle zur Verifikation verteilter Systeme

    23rd Apr 2015 11:14:am
    Venue:

  • AutoMathA 2015

    6th May 2015
    Venue:

    Jewels of Automata: from Mathematics to Applications Leipzig, May 6-9, 2015 The conference AutoMathA 2015 will survey a wide picture of research in automata theory and related mathematical fields. It will consist of 26 invited lectures which will describe significant progress over the past years, and will be a meeting point for both young and...

  • Simon Lessenich: Counting Logics and Games with Counters

    13th May 2015 2:00:pm
    Venue: Raum 9U09

    Referent: Dipl.-Inform. Simon Lessenich Titel: Counting Logics and Games with Counters Abstract: In verification and synthesis, properties or models of interest are often quantitative, and many quantitative aspects involve counting. For example, one might be interested in the amount of memory required by a system, how many simultaneous requests a system has to process along...

  • Presentation Christian Meirich

    20th May 2015 10:00:am
    Venue: Room 5052

  • Presentation: Christian Meirich

    20th May 2015 10:15:am
    Venue: Room 5052

    Optimization of Railway-networks The background of this talk is the motivation to optimize the capacitive load in the field of railway operation research. Especially there are approaches of the strategic network planning in the field of the (German) Federal Transport Infrastructure Plan. A plan like this is a comprehensive compilation of the German government for...

  • Abschlussveranstaltung Graduiertenkolleg AlgoSyn

    17th Jun 2015
    Venue: Room 9222, E3

    Abschlussveranstaltung Graduiertenkolleg AlgoSyn       10.00 Begrüßung 10.15 Präsentation Rückblick auf 9 Jahre AlgoSyn 11.00 Vortrag Sascha Geulen: Learning-based Control Strategies for Hybrid Electric Vehicles 12.00 Vortrag Johanna Nellen: simulation results of learning-based control strategies 13.00 Mittagspause 13.30 Koordination der Abschlussarbeiten und Einteilung der Untergruppen 14.15 Das GK-intere Projekt „Scientific Life“ 14.45 Präsentation „Das Modell Graduiertenkolleg als...

  • Presentation: Rupak Majumdar

    19th Jun 2015 3:00:pm
    Venue: Room 9222, E3

    Algorithmic Formal Methods in Continuous Control Abstract: Algorithmic formal methods such as model checking and reactive synthesis were originally developed in the context of discrete systems such as hardware circuits and software. Over the last few years, these techniques have played an increasingly important role in the development of high assurance cyber-physical systems, in which...

  • Dr. Jan Oliver Ringert, Tel Aviv University, Israel:On Challenges in Reactive Synthesis for Software Engineers: Support for LTL Specification Patterns and a Case Study

    8th Sep 2015 1:00:pm
    Venue:

    Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. Despite recent advancements on the theory and algorithms of reactive synthesis, many challenges remain in bringing reactive synthesis technologies to the hands of software engineers. GR(1) is a well-known fragment of linear temporal logic introduced by Piterman et al....

  • Friedrich Gretz: Semantics and Loop Invariant Synthesis for Probabilistic Programs

    25th Sep 2015 10:00:am
    Venue: Room 9222, E3

    Referent: Dipl.-Inform. Friedrich Gretz Titel: Semantics and Loop Invariant Synthesis for Probabilistic Programs Abstract: In this thesis we consider sequential probabilistic programs. Such programs are a means to model randomised algorithms in computer science. They facilitate the formal analysis of performance and correctness of algorithms or security aspects of protocols. We develop an operational semantics...

Events in 2014

  • Presentation Christian Meirich: Capacity of a railway network

    15th Jan 2014 10:00:am
    Venue: Room 5052

    On behalf of the German Railway Authority (Eisenbahnbundesamt) the suitability of a parameter “Capacity of railway infrastructure” in the target and performance agreement (LuFV) between the federal government and Deutsche Bahn AG has been analyzed. Today the capacity of railway lines can be calculated as well as the capacity of railway nodes by means of...

  • project “Mechanisms of scientific life”

    5th Feb 2014 10:00:am
    Venue: Room 5052

    Presentation of the first results an next steps

  • AlgoSyn-Workshop together with GK PUMA (Programm- Und Modell-Analyse, TU LMU)

    26th Mar 2014 11:00:am
    Venue:

    1st Day, 26.03.2014 10.30  Bus Departure (Entrance Parkinglot Mies-van-der-Rohe-Str.) 12:30 Lunch at Bonn-Aachen International Center for Information Technology B-IT; Dahlmannstraße 2; D-53113 Bonn 14.00 Presentation by the representative H. Seidl und W. Thomas 14.30- 15.45 Short presentations from Aachen (7 min) 15.45 – 16.00 Coffee Break 16.00 – 17.15 Short presentations from Munich (5 – 10 min)...

  • Benedikt Brütsch: Synthesizing Structured Reactive Programs: How Much Memory Do They Need?

    23rd Apr 2014 10:00:am
    Venue: Room 5052

    Benedikt Brütsch: “Synthesizing Structured Reactive Programs: How Much Memory Do They Need?”. Abstract: Existing approaches to the synthesis of controllers in reactive systems typically involve the construction of transition systems such as Mealy automata. In 2011, Madhusudan proposed structured programs over a finite set of Boolean variables as a more succinct formalism to represent the...

  • Visit the Railway Signalling Lab (ELVA) of the Institute of Transport Science

    7th May 2014 10:00:am
    Venue: Room 5052

    Visit the Railway Signalling Lab (ELVA) of the Institute of Transport Science. “Synthesizing Structured Reactive Programs: How Much Memory Do They Need?”. The meeting point will be in the foyer of the building of civil engineering (Mies-van-der-Rohe-Straße 1) at 10.15 a. m.. The AlgoSyn members starting from the Informatikzentrum will meet in front of room...

  • Benjamin Kaminski: Analyzing Expected Outcomes and Almost-Sure Termination of Probabilistic Programs is Hard

    28th May 2014 10:00:am
    Venue: Room 5052

    We consider the hardness of computing expected outcomes and almost-sure termination of probabilistic programs. We show that deciding almost-sure termination and deciding whether the expected outcome of a program equals a given rational value is $\Pi^0_2$-complete. Computing lower and upper bounds on the expected outcome is shown to be recursively enumerable and $\Sigma^0_2$-complete, respectively.

  • Ibtissem Ben Makhlouf and Sarah Winter: Presentation of their work

    2nd Jul 2014 10:00:am
    Venue: Room 5052

    Ibtissem Ben Makhlouf: Reachability Analysis of Hybrid Systems Using Geometric Approximations Hybrid systems combine discrete events and continuous behaviors in the same framework. The discrete part is represented as transitions between locations, in which the continuous part is described as a differential equation and that generally in a confined invariant domain. The transitions are commonly...

  • Christina Jansen: Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs

    16th Jul 2014
    Venue: Room 5052

    Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs   Separation Logic (SL) is an extension of Hoare Logic that supports reasoning about pointer-manipulating programs. It employs inductively-defined predicates for specifying the (dynamic) data structures maintained at runtime, such as lists or trees. To support symbolic execution, SL introduces abstraction rules that yield symbolic representations...

  • Oliver Göbel: Online Independent Set Beyond the Worst-Case

    6th Aug 2014 10:00:am
    Venue: Room 5052

    Title: Online Independent Set Beyond the Worst-Case Abstract: We investigate online algorithms for maximum independent set on graph classes with bounded inductive independence number $\rho$ like interval and disk graphs with applications to, e.g., task scheduling, spectrum allocation and admission control. In the online setting, nodes of an unknown graph arrive one by one over...

  • Johanna Nellen: A CEGAR Approach for the Reachability Analysis of Sequential Function Charts

    22nd Oct 2014 10:00:am
    Venue: Room 5052

    Johanna Nellen: A CEGAR Approach for the Reachability Analysis of Sequential Function Charts We address the safety analysis of chemical plants controlled by programmable logic controllers (PLCs). We consider sequential function charts (SFCs) for the programming of the PLCs, extended with the specification of the dynamic plant behavior. The resulting hybrid SFC models can be...

  • Presentation of Johanna Nellen

    22nd Oct 2014 10:00:am
    Venue: Room 5052

  • Ufuk Topcu: Correct-By-Construction Control Synthesis for Autonomous Systems

    31st Oct 2014 11:00:am
    Venue:

    Ufuk Topcu: Correct-By-Construction Control Synthesis for Autonomous Systems How can we affordably build trustworthy autonomous, networked systems? Partly motivated by this question, I describe a shift from the traditional “design+verify” approach to “specify+synthesize” in model-based engineering. I then discuss our recent results on automated synthesis of correct-by-construction, hierarchical control protocols. These results account for hybrid...

  • AlgoSyn – FAllWorkshop in Schleiden

    6th Nov 2014
    Venue:

    Jährlicher AlgoSyn-interner Workshop

  • Presentation of Christian Meirich

    26th Nov 2014 10:00:am
    Venue: Room 5052

    Präsentation von Christian Meirich: Erhöhung der Leistungsfähigkeit durch eine optimale Ausnutzung von Kapazitäten des Eisenbahnnetzen Im Eisenbahnwesen beschreibt die Kapazität die zulässige Anzahl an Zugfahrten auf einem Infrastrukturbereich innerhalb eines Zeitfensters. Derzeit ist es nicht möglich die einzelnen Kapazitäten von Eisenbahnstrecken mit denen der Eisenbahnknoten zu verrechnen, da unterschiedliche Rechenansätze hierfür verwendet werden. Somit lassen...

  • Promotionscafé

    11th Dec 2014 3:30:pm
    Venue: Room 9220

    Nach der Promotion in die Industrie Mehr Informationen:  www.informatik.rwth-aachen.de/Promotionscafe/

  • AlgoSyn-Meeting

    7th Jan 2015 10:00:am
    Venue: Room 5052

    Agenda Mechanism of Scientific Life FFM 2015 Election: New Steering Committee

  • Young Researchers Conference

    25th Feb 2015
    Venue:

    Young Researchers Conference “Frontiers of Formal Methods” Aachen, Germany February 25 – 27, 2015   organized by the DFG Research Training Groups AlgoSyn (Algorithmic Synthesis of Reactive and Discrete-Continuous Systems), Aachen PUMA (Program and Model Analysis), München QuantLA (Quantitative Logics and Automata), Dresden & Leipzig SCARE (System Correctness under Adverse Conditons), Oldenburg and the Austrian...

Events in 2013

  • Prof. Dr. Oliver Niggemann: Industrie 4.0 = Industrie 3.0 + Wissensverarbeitung?

    24th Jul 2013 10:00:am
    Venue: Room 5052

    Die zunehmende IKT-Integration und neue Anforderungen der Produktionstechnik erhöhen die Komplexität der Automation zunehmend und führen zur Überforderung der Menschen mit damit einhergehender sinkender Arbeitseffektivität. Um dieser Situation zu begegnen hat die Bundesregierung das Thema Industrie 4.0 ins Leben gerufen, welches als zusammenhängendes Forschungsfeld für die Automation aufgefasst werden kann. Durch den Einsatz von intelligenten...

  • Promotionscafé

    23rd Sep 2013 3:00:pm
    Venue:

    Frauen und Männer im Team – gleiche Chancen, gleiche Rechte?! Als Gast wird Frau Dr. Brands, die Gleichstellungsbeauftragte der RWTH Aachen, vortragen. Mehr Informationen:  www.informatik.rwth-aachen.de/Promotionscafe/

  • Presentation Deni Raco

    24th Sep 2013 5:00:pm
    Venue: Room 2202

  • Presentation Gereon Kremer and Frédéric Reinhardt

    2nd Oct 2013 10:00:am
    Venue:

  • annual AlgoSyn workshop

    9th Oct 2013 11:00:am
    Venue:

    From Wed 9th Oct (departure from Aachen around 11am) to Fri 11th Oct (departure from Dagstuhl in the afternoon) we shall have our annual AlgoSyn workshop, this time in Dagstuhl (instead of Rolduc). All AlgoSyns (doctoral students and professors) are requested to do their registration. Schedule

  • AlgoSyn Fall School

    23rd Oct 2013
    Venue:

    AlgoSyn Fall School (October 23rd – 25th, associated with SAGT 2013)   Part A: Algorithmic Game Theory, Mechanism Design, Auction Systems Lectures on Computational Complexity in Games and Auctions by Constantinos Daskalakis (Massachusetts Institute of Technology) Lectures on Linear programming and Mechanism Design by Rakesh Vohra (Kellog School of Management)     Part B: Games and...

  • Presentation Matteo Mio

    13th Nov 2013 10:00:am
    Venue: E3 Room 2.22

    First Talk: Game Semantics for Probabilistic mu-Calculi In this talk I will consider several probabilistic (or quantitative) variants of Kozen’s Modal mu-Calculus, designed for expressing properties of probabilistic-nondeterministic transition systems. Two type of semantics can be defined for these logics: one denotational and one based on a novel kind of games which I call Tree...

  • Presentation Matteo Mio

    14th Nov 2013 10:00:am
    Venue: E3 Room 2.22

    Second Talk: Semantic Foundations of Quantitative (real-valued) Logics based on Functional Analysis Abstract: Several notions of bisimulation for Probabilistic Nondeterministic Transition Systems (PNTS) have been proposed in the literature. I will develop the theory of what I call “Upper-Expectation bisimilarity” using standard results of linear algebra and functional analysis and provide strong mathematical foundations for...

  • Presentation Namit Chaturvedi: Languages of Infinite Traces and Deterministic Asynchronous Automata

    27th Nov 2013
    Venue:

    Abstract: In the theory of deterministic automata for languages of infinite words, a fundamental result relates the family of infinitary limits of regular languages and the family of omega-languages recognized by deterministic Buechi automata. Furthermore, a theorem due to L. Landweber states that an omega-regular language is recognized by a deterministic Buechi automaton if and...

  • Presentation Friedrich Gretz

    11th Dec 2013
    Venue:

  • Presentation Friedrich Gretz

    12th Dec 2013
    Venue: E3 room 2.22 (2nd floor)