+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 14. Dezember 2018, 13:00 Uhr
Ort: Gebäude E3, Seminarraum 9222, Ahornstr. 55
Referent: Ulrich Loup
Theory of Hybrid Systems Informatik 2
Thema: On Solving Real-algebraic Formulas in a Satisfiability-modulo-theories
Framework
Abstract:
Quantifier-free real-algebraic formulas are Boolean combinations of polynomial
equations and inequalities over the domain of the real numbers. Coming with a
strong expressiveness and a still decidable satisfiability problem, real-
algebraic formulas are a precious modeling language in many academic,
industrial and commercial areas. However, only some classes of real-algebraic
formulas allow an efficient solving in practice. For instance, conjunctions of
linear real-algebraic constraints can be solved with the very successful
simplex method.
The general quantifier-free real-algebraic satisfiability problem, however,
has a worst-case time complexity bound which is exponential in the number of
input variables. Methods solving this general problem directly are often
inefficient in practice. The very popular cylindrical algebraic decomposition
(CAD) method has a doubly-exponential complexity bound in the number of input
variables for its search space.
This thesis tackles the solving of general quantifier-free real-algebraic
formulas with a combination of different methods in a satisfiability-modulo-
theories (SMT) framework: A SAT solver computes partial assignments for the
Boolean structure of the real-algebraic formula and real-algebraic solvers
check these assignments for consistency in the real domain. If the assignment
is infeasible in the real domain, the SAT solver would profit from a small -
preferably minimal - reason for this conflict in terms of a subset of the
constraints corresponding to the conflicting assignment.
In this talk, I focus on two real-algebraic solvers in our SMT-solving
framework SMT-RAT, which are major contributions of my thesis. The first
solver is an implementation of the CAD method specialized for an efficient
embedding into an SMT solver. In particular, the CAD method is extended by the
ability to solve incrementally, i.e. reuse pre-computed results, to backtrack
and to compute minimal reasons. Moreover, bounds to the variables are used to
prune the CAD search space, especially when combining the method with
interval-arithmetic techniques.
The second solver uses an extension of Buchberger's algorithm in order to
compute a Gröbner basis. The solver supports incremental solving, backtracking
and minimal reasons for some unsatisfiable cases, as well. We extended the
method so that the solver can also be used in order to simplify formulas for
other real-algebraic solvers in the SMT-solving framework.
As a main part, my thesis comprises an evaluation of the two solvers in the
SMT-RAT framework. In particular, the effects of combining the CAD method with
a Gröbner-bases solver in an SMT framework are investigated.
In my talk, some experimental results of this evaluation are shown, too.
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Dienstag, 11. Dezember 2018, 16:15 Uhr
Ort: Gebäude E3, Seminarraum 9222, Ahornstr. 55
Referent: Florian Frohn, M.Sc.
Lehr- und Forschungsgebiet Informatik 2
Thema: Automated Complexity Analysis of Rewrite Systems
Abstract:
Besides functional correctness, one of the most important prerequisites for
the success of software is efficiency: The desired results need to be
computed not only correctly, but also in time. Thus, analyzing the runtime
complexity of software is indispensable in practice. Unfortunately,
analyzing the complexity of large programs manually is infeasible. Hence,
automated complexity analysis techniques are needed. In this way,
performance pitfalls can be highlighted automatically like other bugs which
can nowadays be found by compilers or static analyzers.
However, statically analyzing the complexity of real-world programs poses
several problems. For example, most programming languages lack formal
semantics. Moreover, different programming languages offer different
features, so static analyses for one language do not necessarily apply to
others. A common solution for these problems is to transform programs into
low-level formalisms like integer or term rewrite systems that can be
analyzed without worrying about language-specific peculiarities.
State-of-the-art tools that analyze the worst-case complexity of rewrite
systems are restricted to the inference of upper bounds. In this talk, the
first techniques for the inference of lower bounds on the worst-case
complexity of integer and term rewrite systems are introduced. While upper
bounds can prove the absence of performance-critical bugs, lower bounds can
be used to find them.
For term rewriting, the power of the presented technique gives rise to the
question whether the existence of a non-constant lower bound is decidable.
Thus, the corresponding decidability results are also discussed in this
talk.
Es laden ein: Die Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 7. Dezember 2018, 10.00 Uhr
Ort: IT Center Seminarraum 004, Kopernikusstr. 6
Referent: Dipl.-Ing. Markus Towara
Informatik 12: Software and Tools for Computational
Engineering
Thema: Discrete Adjoint Optimization with OpenFOAM
Abstract:
Computer simulations and computer aided design in the past decades have
evolved into a valuable instrument, penetrating just about every branch
of engineering in industry and academia.
More specifically, computational fluid dynamics (CFD) simulations allow
to inspect flow phenomena in a variety of applications.
As simulation methods evolve, mature, and are adopted by a rising number
of users, the demand for methods which not only predict the result of a
specific configuration, but can give indications on how to improve the
design, increases.
This thesis is concerned with the efficient calculation of sensitivity
information of CFD algorithms, and their application to numerical
optimization.
The sensitivities are obtained by applying Algorithmic Differentiation (AD).
A specific emphasis of this thesis is placed on the efficient
application of adjoint methods, including parallelism, for commonly used
CFD finite volume methods (FVM) and their implementation in the open
source framework OpenFOAM.
Es laden ein: Die Dozenten der Informatik
** Terminänderung **
************************************************************************
*
* Einladung
*
*
* Informatik-Oberseminar
*
*
************************************************************************
Zeit: Freitag, 14.12.2018, 10.00 Uhr
Ort: Gebäude E3, Seminarraum 9222, Ahornstr. 55
Referent: Herr Arham Muslim, M.Sc.
Titel: OpenLAP: A User-Centered Open Learning Analytics Platform
Abstract:
During the last few years, Learning Analytics (LA) has gained the interest of researchers in the field of Technology Enhanced Learning (TEL). Generally, LA deals with the development of methods that harness educational data sets to support the learning process. It shares a movement from data to analysis to action to learning. Recently, the demand for self-organized, networked, and lifelong learning opportunities has increased. Therefore, there is a need to provide an understanding of how different learners learn in these open learning settings and how learners, educators, institutions, and researchers can best support this process. Moreover, this openness should be reflected in the conceptualization and development of innovative LA approaches in order to achieve more effective learning experiences. Open Learning Analytics (OLA) is an emerging research field that has the potential to deal with these challenges in open learning environments. However, the concrete solutions and implementations that can deliver an effective and efficient OLA are still lacking. Most solutions currently available does not continuously involve end-users in the LA process and follow design patterns which make it difficult to adopt new user requirements. Furthermore, the available implementations are designed and developed for specific scenarios, which address the requirements of a specific set of stakeholders by relying on a predefined set of questions and indicators. These limitations restrict the scope of such solutions and implementations in the context of OLA targeting various stakeholders with different needs.
The aim of this dissertation is to introduce personalization in the LA process by investigating the design of an effective user-centered Open Learning Analytics Platform (OpenLAP) and providing its conceptual, implementation, and evaluation details. OpenLAP provides a user-friendly interface that supports an interactive, exploratory, and real-time user experience to allow the end-users to dynamically define new indicators that meet their goals. Moreover, OpenLAP is designed to be modular and extensible allowing easy integration of new data sources, analytics methods, and visualization techniques at runtime to adopt the new requirements of multiple stakeholders and deliver an ecosystem for OLA. The main contributions of this dissertation include (1) a comprehensive analysis of the currently available LA tools and solutions with respect to their support for openness and personalization, (2) a theoretically sound design of a user-centered OpenLAP based on the requirements gathered from the empirical analysis of the literature, (3) a concrete implementation of OpenLAP providing an interface to self-define the indicators and an extensible mechanism to easily integrated new data sources, analytics methods, and visualization techniques, and (4) a thorough evaluation of OpenLAP in a pilot study at RWTH Aachen University to assess it in terms of usability, usefulness, extensibility, and modularity.
Es laden ein: Die Dozenten der Informatik
Lehr- und Forschungsgebiet Informatik 9
************************************************************************
*
* Einladung
*
*
* Informatik-Oberseminar
*
*
************************************************************************
Zeit: Freitag, 30.11.2018, 11.00 Uhr
Ort: Gebäude E3, Seminarraum 9222, Ahornstr. 55
Referent: Herr Arham Muslim, M.Sc.
Titel: OpenLAP: A User-Centered Open Learning Analytics Platform
Abstract:
During the last few years, Learning Analytics (LA) has gained the interest of researchers in the field of Technology Enhanced Learning (TEL). Generally, LA deals with the development of methods that harness educational data sets to support the learning process. It shares a movement from data to analysis to action to learning. Recently, the demand for self-organized, networked, and lifelong learning opportunities has increased. Therefore, there is a need to provide an understanding of how different learners learn in these open learning settings and how learners, educators, institutions, and researchers can best support this process. Moreover, this openness should be reflected in the conceptualization and development of innovative LA approaches in order to achieve more effective learning experiences. Open Learning Analytics (OLA) is an emerging research field that has the potential to deal with these challenges in open learning environments. However, the concrete solutions and implementations that can deliver an effective and efficient OLA are still lacking. Most solutions currently available does not continuously involve end-users in the LA process and follow design patterns which make it difficult to adopt new user requirements. Furthermore, the available implementations are designed and developed for specific scenarios, which address the requirements of a specific set of stakeholders by relying on a predefined set of questions and indicators. These limitations restrict the scope of such solutions and implementations in the context of OLA targeting various stakeholders with different needs.
The aim of this dissertation is to introduce personalization in the LA process by investigating the design of an effective user-centered Open Learning Analytics Platform (OpenLAP) and providing its conceptual, implementation, and evaluation details. OpenLAP provides a user-friendly interface that supports an interactive, exploratory, and real-time user experience to allow the end-users to dynamically define new indicators that meet their goals. Moreover, OpenLAP is designed to be modular and extensible allowing easy integration of new data sources, analytics methods, and visualization techniques at runtime to adopt the new requirements of multiple stakeholders and deliver an ecosystem for OLA. The main contributions of this dissertation include (1) a comprehensive analysis of the currently available LA tools and solutions with respect to their support for openness and personalization, (2) a theoretically sound design of a user-centered OpenLAP based on the requirements gathered from the empirical analysis of the literature, (3) a concrete implementation of OpenLAP providing an interface to self-define the indicators and an extensible mechanism to easily integrated new data sources, analytics methods, and visualization techniques, and (4) a thorough evaluation of OpenLAP in a pilot study at RWTH Aachen University to assess it in terms of usability, usefulness, extensibility, and modularity.
Es laden ein: Die Dozenten der Informatik
Lehr- und Forschungsgebiet Informatik 9
This event has been canceled.
Title: The Probabilistic Model Checker Storm -- Symbolic Methods for
Probabilistic Model Checking
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Montag, 3. Dezember 2018, 15.00 Uhr
Ort: Gebäude E3, Raum 9007, Ahornstr. 55
Referent: Dipl.-Inform. Christian Hensel
Thema: The Probabilistic Model Checker Storm -- Symbolic Methods for
Probabilistic Model Checking
Abstract:
In a world in which we increasingly rely on safety critical systems that
simultaneously are becoming ever more complex, formal methods provide a
means to mathematically rigorously prove systems correct. Model checking is
a fully aut...
When: Mon Dec 3, 2018 15:00 – 16:00 Central European Time - Berlin
Where: Gebäude E3, Raum 9007, Ahornstr. 55
Calendar: vortraege(a)informatik.rwth-aachen.de
Who:
(Guest list has been hidden at organizer's request)
Invitation from Google Calendar: https://www.google.com/calendar/
You are receiving this courtesy email at the account
vortraege(a)informatik.rwth-aachen.de because you are an attendee of this
event.
To stop receiving future updates for this event, decline this event.
Alternatively you can sign up for a Google account at
https://www.google.com/calendar/ and control your notification settings for
your entire calendar.
Forwarding this invitation could allow any recipient to modify your RSVP
response. Learn more at
https://support.google.com/calendar/answer/37135#forwarding
You have been invited to the following event.
Title: The Probabilistic Model Checker Storm -- Symbolic Methods for
Probabilistic Model Checking
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Montag, 3. Dezember 2018, 15.00 Uhr
Ort: Gebäude E3, Raum 9007, Ahornstr. 55
Referent: Dipl.-Inform. Christian Hensel
Thema: The Probabilistic Model Checker Storm -- Symbolic Methods for
Probabilistic Model Checking
Abstract:
In a world in which we increasingly rely on safety critical systems that
simultaneously are becoming ever more complex, formal methods provide a
means to mathematically rigorously prove systems correct. Model checking is
a fully aut...
When: Mon Dec 3, 2018 15:00 – 16:00 Central European Time - Berlin
Where: Gebäude E3, Raum 9007, Ahornstr. 55
Calendar: vortraege(a)informatik.rwth-aachen.de
Who:
* michaelcochez(a)gmail.com - organizer
* bibliothek(a)informatik.rwth-aachen.de
* infprof(a)informatik.rwth-aachen.de
* assistenten(a)informatik.rwth-aachen.de
* dehnert(a)cs.rwth-aachen.de
* webteam(a)informatik.rwth-aachen.de
* vortraege(a)informatik.rwth-aachen.de
Event details:
https://www.google.com/calendar/event?action=VIEW&eid=MGpsNGhjNXQycnZsaGx0a…
Invitation from Google Calendar: https://www.google.com/calendar/
You are receiving this courtesy email at the account
vortraege(a)informatik.rwth-aachen.de because you are an attendee of this
event.
To stop receiving future updates for this event, decline this event.
Alternatively you can sign up for a Google account at
https://www.google.com/calendar/ and control your notification settings for
your entire calendar.
Forwarding this invitation could allow any recipient to modify your RSVP
response. Learn more at
https://support.google.com/calendar/answer/37135#forwarding
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Montag, 3. Dezember 2018, 15.00 Uhr
Ort: Gebäude E3, Raum 9007, Ahornstr. 55
Referent: Dipl.-Inform. Christian Hensel
Thema: The Probabilistic Model Checker Storm -- Symbolic Methods for Probabilistic Model Checking
Abstract:
In a world in which we increasingly rely on safety critical systems that simultaneously are becoming ever more complex, formal methods provide a means to mathematically rigorously prove systems correct. Model checking is a fully automated technique that is successfully applied in the verification of software and hardware circuits. Probabilistic model checking extends traditional model checking to deal with systems exhibiting stochastic behavior. As model checking can be simplistically viewed as an exhaustive exploration of the state space of the model under consideration, it suffers from the curse of dimensionality: State spaces grow exponentially in the number of components and variables and they quickly become too large to be effectively manageable, a problem that is typically referred to as state space explosion.
Symbolic methods have helped to alleviate this problem substantially. Rather than considering states and transitions of the system individually, they instead exploit structure in the model and treat sets of states and transitions simultaneously. Model checkers based on symbolic techniques dominate the landscape of hardware and software model checking. In the probabilistic setting, symbolic methods show potential but are arguably not on par with their qualitative counterparts.
In this talk, we summarize our advances in the field of symbolic techniques in the context of probabilistic model checking. After a brief introduction, we show how to reduce probabilistic systems including nondeterministic choices that are represented using decision diagrams with respect to bisimulation minimization, a well-studied technique for factoring out symmetry. Then, we show how to compute and refine bounds on reachability probabilities for infinite-state systems before presenting our novel probabilistic model checker Storm, which encompasses the aforementioned techniques and significantly outperforms competing tools on a set of standard benchmarks.
Es laden ein: Die Dozenten der Informatik
************************************************************************
**
* Einladung
*
*
* Informatik-Oberseminar
*
*
************************************************************************
Zeit: Montag, 19.11.2018, 16.30 Uhr
Ort: Gebäude E3, Seminarraum 9222
Referentin: Frau Anastassia Küstenmacher, M.Sc.
Titel: Improving the Reliability of Service Robots in the Presence of
External Faults
Abstract:
In the field of domestic service robots, recovery from faults is crucial to
promote user acceptance. In this context, this work focuses on some specific
faults which arise from the interaction of a robot with its real world
environment. Even a well-modelled robot may fail to perform its tasks
successfully due to external faults which occur because of an infinite
number of unforeseeable and unmodelled situations.
Through investigating the most frequent failures in typical scenarios which
have been observed in real-world demonstrations and competitions using the
autonomous service robots Care-O-Bot III and youBot, we identified four
different fault classes caused by disturbances, imperfect perception,
inadequate planning operator of chaining of action sequences.
This thesis then presents two approaches to handle external faults caused by
insufficient knowledge about the preconditions of the planning operator.
The first approach presents reasoning on detected external faults using
knowledge about naïve physics. The naïve physics knowledge is represented by
the physical properties of objects which are formalized in a logical
framework. The proposed approach applies a qualitative version of physical
laws to these properties in order to reason. By interpreting the reasoning
results the robot identifies the information about the situations which can
cause the fault. Applying this approach to simple manipulation tasks like
picking and placing objects show that naïve physics holds great
possibilities for reasoning on unknown external faults in robotics.
The second approach includes missing knowledge about the execution of an
action through learning by experimentation. Firstly, it investigates such
representation of executing specific knowledge that can be learned for one
particular situation and reused for situations which deviate from the
original. The combination of symbolic and geometric models allows us to
represent action execution knowledge effectively. This representation is
called action execution model (AEM) here. The approach provides a learning
strategy which uses a physical simulation for generating the training data
to learn both symbolic and geometric aspects of the model. The experimental
analysis, performed on two physical robots, shows that AEM can reliably
describe execution specific knowledge and thereby serving as a potential
model for avoiding the occurrence of external faults.
Es laden ein: Die Dozenten der Informatik
Lehr- und Forschungsgebiet Informatik 5
***********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
***********************************************************************
Zeit: Donnerstag, 22. November 2018, 15:00 Uhr
Ort: Seminarraum 9007, Gebäude E3, Ahornstr. 55
Referent: Dipl.-Inform. Martin Henze
Thema: Accounting for Privacy in the Cloud Computing Landscape
Abstract:
Cloud computing enables service operators to efficiently and flexibly
utilize resources offered by third party providers instead of having to
maintain their own infrastructure. As such, cloud computing offers many
advantages over the traditional service delivery model, e.g., failure
safety, scalability, cost savings, and a high ease of use.
Consequently, cloud computing has revolutionized service delivery and
we observe a tremendous trend for moving services to the cloud.
However, this trend of outsourcing services and data to the cloud is
limited by serious privacy challenges as evidenced by recent security
breaches and privacy incidents. Overcoming these privacy challenges is
key to enable corporate and private users to fully embrace the
advantages of cloud computing.
We argue that overcoming these privacy challenges requires cooperation
between the various actors in the cloud computing landscape, i.e.,
users, service providers, and infrastructure providers. All these
different actors have clear incentives to cater for privacy but often
lack the technical means to do so. To overcome this situation, we
provide technical approaches that enable each of them to account for
privacy. In this talk, we specifically focus on two contributions in
more detail: (i) To support users in exercising their privacy, we raise
their awareness for the exposure to cloud services in the context of
smartphone apps as well as email services and enable them to
anonymously compare their cloud usage to their peers. (ii) By providing
privacy requirements-aware cloud infrastructure, we realize user-
specified per-data-item privacy policies and thus enable infrastructure
providers to adhere to them when storing data in the cloud. Our
contributions highlight that it is both promising and feasible to apply
cooperation of different actors to strengthen users' privacy and
consequently enable more corporate and private users to benefit from
cloud computing.
Es laden ein: Die Dozentinnen und Dozenten der Informatik