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 |
---|---|---|---|---|
15.08.2019 2:00 p.m. | Felix Pauck | Together Strong: Cooperative Android App Analysis (draft presenation, Kuchenseminar) | English | O4.225 |
15.08.2019 2:00 p.m. | Felix Pauck | Past research + Discussion: What should be next (presenation, Kuchenseminar) | English | O4.225 |
Past Talks
Due privacy reasons full names of students will not be displayed.
Date | Speaker | Topic | Language | Room |
---|---|---|---|---|
04.07.2019 2:00 p.m. | Felix Pauck | Android Taint-Analysis Benchmarks: Past, Present and Future (trial presenation, Kuchenseminar) | English | O4.225 |
14.05.2019 1:00 p.m. | Jan Haltermann | Analyzing Data Usage in Array Programs (Master's thesis defense) | English | O4.267 |
07.05.2019 | Cedric Richter | Neural Algorithm Selection for Software Verification (Master's thesis proposal) | English | O4.225 |
16.04.2019 2:00 p.m. | Arnab Sharma | Verification and Validation of Different intriguing properties of Machine Learning Algorithms (Kuchenseminar) | English | O4.225 |
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 | 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 |