Achtung:

Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

Info-Icon Diese Seite ist nicht in Deutsch verfügbar
Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right) Bildinformationen anzeigen

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right)

Group Seminar

The group seminar takes place in 1-2 week intervals during the semester. Talks and discussions cover current research topics of our group as well as bachelor's and master's theses. We cordially invite everyone who is interested to join us.

The language of the talk depends on the speaker. If there is an interesting topic but you are in doubt whether the talk will be in English, feel free to ask Manuel or any other member of our group

Coming Events

Date Speaker Topic Language Room
16.04.2019
2:00 p.m.
Arnab Sharma Verification and Validation of Different intriguing properties of Machine Learning Algorithms (Kuchenseminar) English O4.225

Past Talks

Due privacy reasons full names of students will not be displayed.

 
Date Speaker Topic Language Room
28.03.2019
3:00 p.m.
Cedric Richter PeSCo: Predicting Sequential Combinations of Verifiers (Kuchenseminar) English O4.225
07.02.2019
2:00 p.m.
Arnab Sharma Testing Balances of Machine Learning Algorithms English O4.225
30.01.2019
2:00 p.m.
Steffen Beringer Consistency of AUTOSAR Timing Constraints (Kuchenseminar) English O4.225
24.01.2019
10:30 a.m.
  Verification of Conflict Opacity for Software Transactional Memory Algorithms with Uppaal (Masters'thesis defense) English O4.267
24.01.2019
10:30 a.m.
  Combining Android Apps for Analysis Purposes (Masters'thesis defense) English O4.267
29.11.2018
2:30 p.m.
Jan Haltermann Analyzing Data Usage in Array Programs (Masters'thesis proposal) English O4.267
29.11.2018
2:00 p.m.
  Aktualisierung von veralteten Android Apps mittels Soot (Bachelor's thesis defense) German O4.267
22.11.2018
2:00 p.m.
  Entwicklung und Integration einer quantitativen Informationsflusskontrolle (Bachelors'thesis defense) German O4.267
30.08.2018
14:00 a.m.
  Kuchenseminar English O4.225
30.08.2018
13:00 a.m.
Felix Pauck
Philipp Schubert
Manuel Töws
ComBet English O4.225
09.08.2018
2:00 p.m.
Manuel Töws Domination Validation (Kuchenseminar) English O4.225
13.07.2018
11:00 a.m.
  Combining Android Apps for analysis purposes (Masters'thesis proposal) English O3.267
19.06.2018
2:30 p.m.
  Korrektheitsbeweise für Muster von Servicekompositionen (Bachelors'thesis defense) German O3.267
30.05.2018
1:30 p.m.
  Entwicklung und Integration einer quantitativen Informationsflusskontrolle (Bachelors'thesis proposal) German O4.267
30.05.2018
1:30 p.m.
  Verification of Conflict Opacity for Software Transactional Memory Algorithms with Uppaal (Masters'thesis proposal) English O4.267
23.05.2018
1:00 p.m.
Jürgen König Data Independence for STMs (Kuchenseminar) English O4.225
14.05.2018
1:00 p.m.
  Aktualisierung von veralteten Android Apps mittels Soot (Bachelors'thesis proposal) German O4.267
12.04.2018
2:00 p.m.
  Identifying correlation between program structures and verification performance (Kuchenseminar) English O4.225
11.04.2018
2:00 p.m.
Arnab Sharma Machine Learning Algorithms -Part 2 (Kuchenseminar) English O4.225
15.03.2018
1:00 p.m.
Manuel Töws Hyperproperties and HyperLTL/CTL* - Part 2 (Kuchenseminar) English O4.225
21.02.2018
3:00 p.m.
Arnab Sharma Machine Learning Algorithms -Part 1 (Kuchenseminar) English O4.225
27.02.2018
1:00 p.m.
Jürgen König Software Transactional Memory (Kuchenseminar) English O4.225
08.02.2018
1:00 p.m.
Prof. Dr. Heike Wehrheim Reducer-Based Construction of Conditional Verifiers (Kuchenseminar) English O4.225
25.01.2018
13:30 a.m.
Felix Pauck Reprodroid (Kuchenseminar) English O4.225
11.01.2018
11:00 a.m.
Arnab Sharma Fairness in Machine Learning Software (Kuchenseminar) English O4.225
20.12.2017
2:00 p.m.
  Beweise für die Korrektheit von Softwarekomponenten-Templates unter einem erweitertem Hoare-Kalkül German O2.267
14.12.2017
11:00 a.m.
Manuel Töws Hyperproperties and HyperLTL/CTL* - Part 1(Kuchenseminar) English O4.225
02.11.2017
2:00 p.m.
Manuel Töws Policy Dependent and Independent Information Flow Analyses English O3.267
26.10.2017
1:00 p.m.
  Automatic Contract Validation for Service Compositions (Master's thesis defense) English O3.267
11.10.2017
4:00 p.m.
Jürgen König Value-Based or Conflict-Based? Opacity Definitions for STMs English O4.267
25.09.2017
11:00 a.m.
  (Master's Thesis proposal) English O4.267
11.09.2017
3:00 p.m.
Prof. Dr. Heike Wehrheim Fault Localization in Service Compositions (Kuchenseminar) English O4.225
17.08.2017
02:00 p. m.
  Evolutionäre Strategieberechnung für Timed Game Automata (Bachelor's Thesis defense) German O4.267
13.07.2017
2:30 p.m.
Jürgen König Invariantensuche für RingSTM (Kuchenseminar) English O4.225
06.07.2017
2:00 p.m.
Steffen Beringer Spezifikation von AUTOSAR Timing Constraints (Kuchenseminar) English O4.225
22.06.2017
02:00 p.m.
  Testing Opacity of Software Transactional Memory Algorithms (Bachelor’s Thesis defense) German O4.267
21.06.2017
08:30 a.m.
Felix Pauck Cooperative static analysis of Android applications (Master's thesis defense) English O4.267
23.05.2017
11:00 a.m.
  Automatic Contract Validation for Service Compositions (Master's thesis proposal) English O4.267
18.05.2017
2:00 p.m.
  Korrektheit der Fallstudie FastLane - Beweis einer Verfeinerungsbeziehung zwischen Opacity und FastLane über TMS2 (Master's thesis defense) German O3.267
11.05.2017
3:30 p.m.
Marie-Christine Jakobs Compact Proof Witnesses English O3.267
06.04.2017
1:00 p.m.
Oleg Travkin Kuchenseminar English O4.225
04.04.2017
1:00 p.m.
Marie-Christine Jakobs Kuchenseminar English O4.225
07.03.2017
1:00 p.m.
Manuel Töws Policy Dependent and Independent Information
Flow Analysis (Kuchenseminar)
English O4.225
20.02.2017
02:00 p. m.
  Evolutionäre Strategieberechnung für Timed Game Automata (Bachelor's Thesis Proposal) German O4.267
12.01.2017
02:00 p. m.
  Development and Implementation of a Test Tool for
Conflict Based Opacity in C++ (Bachelor’s Thesis Proposal)
German O4.267
15.12.2016
11:00 a.m.
  Verifikation von Service Kompositionen mit SPIN (Bachelor's thesis defense) German O4.216
15.12.2016
10:30 a.m.
  Korrektheitsüberprüfung von Invariantenkandidaten für nebenläufige Datenstrukturen
(Bachelor's thesis proposal)
German O4.216
15.12.2016
10:00 a.m.
  Vorstellung SeSAME und laufender Arbeiten daran German O4.216
08.12.2016
09:00 a.m.
  Cooperative static analysis of Android applications (Master's thesis proposal) German O4.267
05.12.2016, 02:00 p.m.   Verifikation von Service-Kompositionen mit Prolog (Bachelor's thesis defense) German O4.267
17.11.2016
11:00 a.m.
  Korrektheit der Fallstudie FastLane - Beweis einer Verfeinerungsbeziehung zwischen Opacity und FastLane über TMS2 German O4.267
10.11.2016
02:00 p.m.
Manuel Töws A CEGAR Scheme For Information Flow Analysis English O4.267
10.11.2016
02:00 p.m.
Manuel Töws PAndA2 : Analyzing Permission Use and Interplay in Android Apps English O4.267
15.09.2016
2 p.m.
Steffen Beringer Verification of AUTOSAR Software Architectures with Timed Automata English O4.267
21.07.2016
3 p.m.
Marie-Christine Jakobs Kuchenseminar English O4.267
29.06.2016
2 p.m.
Julia Krämer A Formal Approach to Error Localisation and Correction in Service Compositions English O4.267
16.06.2016
2 p.m.
Manuel Töws On checking information flow in Service Compositions (Kuchenseminar) English O4.225
09.06.2016, 2 p.m.   Verifikation von Service-Kompositionen mit Prolog (Bachelor's thesis proposal) German O4.267
09.06.2016, 2 p.m.   Verifikation von Service-Kompositionen mit Spin (Bachelor's thesis proposal) German O4.267
09.06.2016, 2 p.m.   Fehlersuche in Service-Kompositionen mit MaxSMT (Bachelor's thesis proposal) German O4.267
25.04.2016, 1 p.m.   Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung (Bacherlor's thesis' defense talk)   O4.267
04.07.2016 A^3: Android App Analysis Final Presentation of Project Group A^3: Android App Analysis English O4.267
18.02.2016, 2.45 p.m. Marie-Christine Jakobs Just test what you cannot verify!   O4.267
18.02.2016, 2 p.m.   Predicting Rankings of Software Verification Tools Using Kernels for Structured Data (Master's thesis defense)   O4.267
21.01.2016, 2 p.m.   Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions (Master's thesis defense)   O4.267
14.12.2015 A^3: Android App Analysis Second Milestone Presentation of Project Group A^3: Android App Analysis English O4.267
18.11.2015, 2 p.m. Steffen Beringer Specification and Verification of AUTOSAR Timing Requirements   O3.267
11.11.2015, 11 a.m. Oleg Travkin TSO to SC via symbolic execution   O4.225
20.10.2015, 11:00 a.m.   Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung (Bachelor's thesis proposal talk)   O3.267
Thu, 03.09.2015, 9 a.m. Marie-Christine Jakobs Speed Up Configurable Certificate Validation by Certificate Reduction And Partioning   O4.267
Mo, 31.08.2015, 5 p.m.   Evaluierung von Prozessmanagementlösungen im Hinblick auf agile Prozesse (Bacherlor's thesis' defense talk)   O4.267
Tue, 14.07.2015, 2 p.m.   Program Slicing: A Way of Separating C Programs into Approximate and Precise Portions (Master's thesis proposal)   O4.267
Tue, 16.06.2015, 3 p.m. Tobias Isenberg Incremental Inductive Verification of Parameterized Timed Systems   O4.267
11.06.2015, 3 p.m. Julia Krämer Error Localization in Service Compositions   O4.267
21.05.2015, 3 p.m.   Evaluierung vonProzessmanagementlösungen im Hinblick auf agile Prozesse (Bachelor's thesis proposal talk)   O4.267
21.05.2015, 3.30 p.m. Marie-Christine Jakobs How to speed up Configurable Software Certification?   O4.267
21.05.2015, 4 p.m.   A Survey on Data-driven Software Analysis   O4.267
07.05.2015, 3 p.m. Sven Walther Termination Function Discovery in Service Compositions   O4.267
30.04.2015, 3 p.m. Oleg Travkin Programmverifikation unter TSO   O4.267
16.04.2015, 3 p.m. Manuel Töws Enforcing of algebra-based flow policies   O4.267
09.04.2015, 3 p.m. Marie-Christine Jakobs Programs from Proofs of Predicated Dataflow Analyses   O4.267
09.04.2015, 3.45 p.m.   Just test what you cannot verify!   O4.267
22.01.2015, 2 p.m. Julia Krämer Attack-Defence Graphs - eine formale Sprache für sicherheitskritische Systeme   O3.267
15.01.2015, 2 p.m. Steffen Ziegert Durative Graph Transformations with Required Concurrency and Urgency   O3.267
20.11.2014, 3 p.m.   Ein hierarchischer Ansatz für temporale Planung bei erforderlicher Nebenläufigkeit (Bachelor's thesis defense)   O4.267
20.11.2014, 3:30 p.m.   Untersuchung transitiver Eigenschaften der Technik "Programs from Proofs" (Bachelor's thesis defense)   O4.267
13.11.2014, 10 a.m. Oleg Travkin Handling TSO in Mechanized Linearizability Proofs   O4.267
13.11.2014, 11 a.m. Steffen Beringer Visuelle Spezifikation und Analyse von Anforderungen im Kontext der Steuergeräteentwicklung mit AUTOSAR   O4.267
30.10.2014, 2 p.m. Tobias Isenberg Timed Automata Verification via IC3 with Zones   O4.267
23.10.2014, 2 p.m.   Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren (Bachelor's thesis defense)   O4.267
24.09.2014, 2 p.m.   Visualisierung von SMT-Solver-Ausgaben (Bachelor's thesis defense)   O4.267
04.09.2014, 2 p.m. Sven Walther Verified Service Compositions by Template-based Construction   O4.267
21.08.2014, 2 p.m.   Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen in SMT-LIB (Master's thesis defense)   O4.267
21.08.2014, 2.45 p.m.   Entwicklung eines Konzepts zur Kodierung eines objektorientierten Typsystems in SMT (Bachelor's thesis defense)   O4.267
20.08.2014, 2 p.m. Galina Besova Grammar-based Model Transformations   O4.267
20.08.2014, 2.45 p.m. Sven Walther Towards Systematic Configuration for Architecture Validation   O4.267
16.07.2014, 2 p.m. Marie-Christine Jakobs Certification for Configurable Program Analysis   O3.267
16.07.2014, 2.45 p.m. Monika Wedel Linearisierbarkeitsbeweis der Work-Stealing Deque (Bachelor's thesis defense)   O3.267
11.06.2014, 2 p.m.   Integration von History-basierten Korrektheits-Checks im Model Checker SPIN (Bachelor's Thesis defense)   O4.267
28.05.2014, 2 p.m.   Formal Semantics of Probabilistic SMT Solving in Verification of Service Compositions (Master's Thesis defense)   O3.267
28.05.2014, 2.30 p.m.   Untersuchung transitiver Eigenschaften von Programs from Proofs (Bachelor's Thesis proposal talk)   O3.267
14.05.2014, 2 p.m.   Transformation graphischer Protokollspezifikationen in Model-Checker-Anfragen (Bachelor's Thesis defense)   O3.267
14.05.2014, 2.30 p.m.   Ein hierarchischer Ansatz für temporale Planung bei erforderlicher Nebenläufigkeit (Bachelor's Thesis proposal talk)   O3.267
13.03.2014, 2 p.m.   Generierung von Eigenschaftsprüfern in einem HW/SW-Co-Verifikationsverfahren (BA proposal talk)   O4.267
05.03.2014, 2 p.m.   Collaborative Verification and Testing with Explicit Assumptions   O4.267
05.03.2014, 2.30 p.m.   Visualisierung von SMT-Solver-Ausgaben (BA proposal talk)   O4.267
19.02.2014   Entwicklung eines Konzepts zur Kodierung eines objektorientierten Typsystems in SMT   O4.267
19.02.2014   Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen in SMT-LIB   O4.267
30.01.2014 Steffen Ziegert Real-Time Planning on Temporal Multi-Agent Domains   O4.267
09.01.2014 Tobias Isenberg Proof-Carrying Hardware via IC3   O4.267
09.01.2014   Linearisierbarkeitsbeweis der Work-Stealing Double-Ended Queue   O4.267
19.12.2013 Marie-Christine Jakobs Simplify Verification by Program Transformation   O4.267
09.12.2013   Formal Semantics of Probabilistic SMT Solving in Verification of Service Compositions (Master Thesis, proposal presentation)   O3.267
09.12.2013   Vergleichsstudie zur Ausdrucksstärke von SMT-Solvern (Bachelor Thesis defense, in German)   O3.267
09.12.2013   Introduction to Fuzzy Temporal Logic (Seminar: Probabilistic Methods in Verification)   O3.267
05.12.2013 Steffen Beringer Timing Analysis of AUTOSAR Software Architectures using Timed Automata   O4.267
28.11.2013 Sven Walther Coping with quantification in SMT-based verification of service compositions. A discussion.   O4.267
20.11.2013   BA-Antrittsvortrag: Transformation graphischer Protokollspezifikationen in Model-Checker-Anfragen   O4.267
07.11.2013 Galina Besova Grammar-based Model Transformations   O4.267
31.10.2013 Oleg Travkin SPIN as a linearizability checker under weak memory models   O4.267
24.10.2013 Dominik Steenken SMT Solving for Embedding Feasibility in Lazy State Space Construction for Abstract Graph Transformation   O4.267
24.10.2013   Analyse von Benutzeranforderungen von Service-Kompositionen mittels Modelchecking   O4.267
30.09.2013   Generierung von Promela-Modellen aus Implementierungen von nebenläufigen Datenstrukturen in Form von LLVM IR   O4.267
10.07.2013 Sven Walther Knowledge-based Verification of Service Compositions - an SMT Approach   O4.267
04-07.2013 Dominik Steenken Predicate Mining in Graph Traces via Interpolation   O4.267
27.06.2013 Oleg Travkin Programmspezifikation für Linearisierbarkeitsbeweise unter schwachen Speichermodellen   O4.267
19.06.2013 Alexander Schremmer Towards CEGAR of separation logic domains based on multi-parametric precisions   O4.267
06.06.2013 Marie-Christine Jakobs Certification for Configurable Program Analysis   O2.267
29.05.2013   Bachelor Thesis: Berechnung von Memory-Model-spezifischen Kontrollflussgraphen   O4.267
29.05.2013 Tobias Isenberg Bounded Model Checking of Graph Transformation Systems via SMT Solving   O4.267
22.05.2013 Steffen Ziegert Multilevel Planning for Self-Optimizing Mechatronic Systems   O4.267
16.05.2013 Sven Walther Generating Loop Invariants using Templates   O4.267
15.05.2013 Steffen Beringer AUTOSAR   O4.267
18.04.2013 Tobias Isenberg Inductive Methods   O4.267
21.03.2013   Dreiwertiges Model Checking paralleler Systeme mit heuristisch geleiteter Generierung von Gegenbeispielen   O3.267
11.03.2013   Combining Three-Valued Logic and Quantified Boolean Formulae in Bounded Model Checking Encodings   O4.267
07.02.2013 Steffen Ziegert Durative Graph Transformations: Semantics and Properties   O2.267
29.01.2013   Multiagenten-Koordination in temporaler Planung   O3.267
29.01.2013 Alexander Schremmer Separation Logic meets CEGAR   O3.267
28.01.2013   Suchraumeinschränkung für Graphgrammatiken durch temporallogische Formeln   O2.267
23.01.2013   Ein Tool zur automatischen Generierung von Graphabstraktionen   O4.267
10.01.2013 Oleg Travkin Towards Memory-Model-aware Semantics for High Level Languages   O3.267
20.12.2012 Sven Walther A Primer on Description Logics   O3.267
19.12.2012   Exploiting Planning Graphs and Landmarks for Efficient GTS Planning   O4.267
13.12.2012 Dominik Steenken
+SHK
Counterexample Analysis via Shape Constraints
Abstraction Maintenance and Counterexample Analysis in SGA
  O3.267
29.11.2012   Memory Model-Aware Model Checking 
A Library of Platform Models for Model Weaving and Verification
  O3.267
22.11.2012 Galina Besova Generic and Domain Specific Method Engineering   O4.267
08.11.2012 Nils Timm Heuristic-Guided Abstraction Refinement for Concurrent Systems   O4.267
18.10.2012 Tobias Isenberg Bounded Model Checking für Graphtransformationssysteme als SMT-Problem   O4.267
26.09.2012 Galina Besova Weaving-Based Configuration and Modular Transformation of Multi-Layer Systems   O4.267
25.07.2012 Steffen Ziegert Approaches to Cooperative Pathfinding   O4.267
11.07.2012 Sven Walther Generic Reasoning about Specific Domains   O4.267
28.06.2012 Nils Timm Heuristic-Guided Abstraction Refinement for Concurrent Systems   O4.267
11.06.2012 Oleg Travkin Linearisierbarkeit anhand lokaler Beweisverpflichtungen - Fallstudie: Multiset   O4.267
04.06.2012 Alexander Schremmer Abstraction Refinement in UFO   O4.267
10.05.2012 Dominik Steenken Ein Konzept für eine vollautomatische Erreichbarkeitsanalyse für Shape Graphen   O4.267
03.05.2012 Thomas Ruhroth Modeling and Verification of Secure Information Flow Properties in UMLsec- Models   O4.267
12.04.2012 Galina Besova Model-driven Development of Model Transformations   O4.267
01.02.2012 Daniel Wonisch Proof Simplification by Program Transformation   O4.216
26.01.2012 Sven Walther Avoiding State Space Explosion using Pairwise Composition   O4.216
12.01.2012 Steffen Ziegert Perspectives in Planning with Graph Transformation   O4.216
08.12.2011 Nils Timm 3-valued Abstraction for (Bounded) Model Checking   O4.216
01.12.2011 Oleg Travkin Multi-Core Memory Models - Eine Einführung   O4.216
17.11.2011 Alexander Schremmer Runtime Verification   O4.216
27.10.2011 Dominik Steenken Word Level Bitvector Interpolation for Verification   O4.216

Die Universität der Informationsgesellschaft