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
Bildinformationen anzeigen

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

DateSpeakerTopicLanguageRoom
20.12.2017
2:00 p.m.
Kai Rautenberg Beweise für die Korrektheit von Softwarekomponenten-Templates unter einem erweitertem Hoare-KalkülGermanO2.267

Past Talks

DateSpeakerTopicLanguageRoom
02.11.2017
2:00 p.m.
Manuel TöwsPolicy Dependent and Independent Information Flow Analyses EnglishO3.267
26.10.2017
1:00 p.m.
Paul BördingAutomatic Contract Validation for Service Compositions (Master's thesis defense)EnglishO3.267
11.10.2017 4:00 p.m.Jürgen KönigValue-Based or Conflict-Based? Opacity Definitions for STMs EnglishO4.267
25.10.2017
11:00 a. m.
Anand Bhat(Master's Thesis proposal)EnglishO4.267
17.08.2017
02:00 p. m.
Cedric RichterEvolutionäre Strategieberechnung für Timed Game Automata (Bachelor's Thesis defense)GermanO4.267
22.06.2017
02:00 p. m.
Stefan Müssemeier Testing Opacity of Software Transactional Memory Algorithms (Bachelor’s Thesis defense)GermanO4.267
21.06.2017
08:30 a.m.
Felix PauckCooperative static analysis of Android applications (Master's thesis defense)EnglishO4.267
23.05.2017
11:00 a.m.
Paul BördingAutomatic Contract Validation for Service Compositions (Master's thesis proposal)EnglishO4.267
18.05.2017
2:00 p.m.
Monika
Wedel
Korrektheit der Fallstudie FastLane - Beweis einer Verfeinerungsbeziehung zwischen Opacity und FastLane über TMS2 (Master's thesis defense)GermanO3.267
11.05.2017
3:30 p.m.
Marie-Christine JakobsCompact Proof Witnesses EnglishO3.267
20.02.2017
02:00 p. m.
Cedric RichterEvolutionäre Strategieberechnung für Timed Game Automata (Bachelor's Thesis Proposal)GermanO4.267
12.01.2017
02:00 p. m.
Stefan Müssemeier Development and Implementation of a Test Tool for
Conflict Based Opacity in C++ (Bachelor’s Thesis Proposal)
GermanO4.267
15.12.2016
11:00 a.m.
Markus DewenderVerifikation von Service Kompositionen mit SPIN (Bachelor's thesis defense)GermanO4.216
15.12.2016
10:30 a.m.
Sven HartwigKorrektheitsüberprüfung von Invariantenkandidaten für nebenläufige Datenstrukturen
(Bachelor's thesis proposal)
GermanO4.216
15.12.2016
10:00 a.m.
Cedric Richter,
Jan
Haltermann
Vorstellung SeSAME und laufender Arbeiten daranGermanO4.216
08.12.2016
09:00 a.m.
Felix PauckCooperative static analysis of Android applications (Master's thesis proposal)GermanO4.267
05.12.2016, 02:00 p.m.Philipp HeinischVerifikation von Service-Kompositionen mit Prolog (Bachelor's thesis defense)GermanO4.267
17.11.2016
11:00 a.m.
Monika
Wedel
Korrektheit der Fallstudie FastLane - Beweis einer Verfeinerungsbeziehung zwischen Opacity und FastLane über TMS2GermanO4.267
10.11.2016
02:00 p.m.
Manuel TöwsA CEGAR Scheme For Information Flow AnalysisEnglishO4.267
10.11.2016
02:00 p.m.
Manuel TöwsPAndA2 : Analyzing Permission Use and Interplay in Android AppsEnglishO4.267
15.09.2016
2 p.m.
Steffen BeringerVerification of AUTOSAR Software Architectures with Timed Automata EnglishO4.267
29.06.2016
2 p.m.
Julia Krämer A Formal Approach to Error Localisation and Correction in Service Compositions EnglishO4.267
09.06.2016, 2 p.m.Philipp HeinischVerifikation von Service-Kompositionen mit Prolog (Bachelor's thesis proposal)GermanO4.267
09.06.2016, 2 p.m.Markus DewenderVerifikation von Service-Kompositionen mit Spin (Bachelor's thesis proposal)GermanO4.267
09.06.2016, 2 p.m.Felix KorfmacherFehlersuche in Service-Kompositionen mit MaxSMT (Bachelor's thesis proposal)GermanO4.267
25.04.2016, 1 p.m.Henrik BröcherEvaluation 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 EnglishO4.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. Mike Czech Predicting Rankings of Software Verification Tools Using Kernels for Structured Data (Master's thesis defense) O4.267
21.01.2016, 2 p.m. Guangli Zhang Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions (Master's thesis defense) 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. Henrik Bröcher 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. Jan Bödefeld Evaluierung von Prozessmanagementlösungen im Hinblick auf agile Prozesse (Bacherlor's thesis' defense talk) O4.267
Tue, 14.07.2015, 2 p.m. Guangli Zhang 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. Jan Bödefeld 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. Mike Czech 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. Mike Czech 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. Johannes Heil Ein hierarchischer Ansatz für temporale Planung bei erforderlicher Nebenläufigkeit (Bachelor's thesis defense) O4.267
20.11.2014, 3:30 p.m. Philipp Korth 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. Felix Pauck Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren (Bachelor's thesis defense) O4.267
24.09.2014, 2 p.m. Sebastian Osterbrink 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. Manuel Töws Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen in SMT-LIB (Master's thesis defense) O4.267
21.08.2014, 2.45 p.m. Andreas Krakau 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. Katharina Dridger Integration von History-basierten Korrektheits-Checks im Model Checker SPIN (Bachelor's Thesis defense) O4.267
28.05.2014, 2 p.m. Maryam Sanati Formal Semantics of Probabilistic SMT Solving in Verification of Service Compositions (Master's Thesis defense) O3.267
28.05.2014, 2.30 p.m. Philipp Korth Untersuchung transitiver Eigenschaften von Programs from Proofs (Bachelor's Thesis proposal talk) O3.267
14.05.2014, 2 p.m. Christoph Klauke Transformation graphischer Protokollspezifikationen in Model-Checker-Anfragen (Bachelor's Thesis defense) O3.267
14.05.2014, 2.30 p.m. Johannes Heil Ein hierarchischer Ansatz für temporale Planung bei erforderlicher Nebenläufigkeit (Bachelor's Thesis proposal talk) O3.267
13.03.2014, 2 p.m. Felix Pauck Generierung von Eigenschaftsprüfern in einem HW/SW-Co-Verifikationsverfahren (BA proposal talk) O4.267
05.03.2014, 2 p.m. Mike Czech Collaborative Verification and Testing with Explicit Assumptions O4.267
05.03.2014, 2.30 p.m. Sebastian Osterbrink Visualisierung von SMT-Solver-Ausgaben (BA proposal talk) O4.267
19.02.2014 Andreas Krakau Entwicklung eines Konzepts zur Kodierung eines objektorientierten Typsystems in SMT O4.267
19.02.2014 Manuel Töws Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen in SMT-LIB O4.267
30.01.2014Steffen ZiegertReal-Time Planning on Temporal Multi-Agent DomainsO4.267
09.01.2014Tobias IsenbergProof-Carrying Hardware via IC3O4.267
09.01.2014Monika WedelLinearisierbarkeitsbeweis der Work-Stealing Double-Ended QueueO4.267
19.12.2013Marie-Christine JakobsSimplify Verification by Program TransformationO4.267
09.12.2013Maryam SanatiFormal Semantics of Probabilistic SMT Solving in Verification of Service Compositions (Master Thesis, proposal presentation)O3.267
09.12.2013Marco EngelbrechtVergleichsstudie zur Ausdrucksstärke von SMT-Solvern (Bachelor Thesis defense, in German)O3.267
09.12.2013Lugman AhmadIntroduction to Fuzzy Temporal Logic (Seminar: Probabilistic Methods in Verification)O3.267
05.12.2013Steffen BeringerTiming Analysis of AUTOSAR Software Architectures using Timed AutomataO4.267
28.11.2013Sven WaltherCoping with quantification in SMT-based verification of service compositions. A discussion.O4.267
20.11.2013Christoph KlaukeBA-Antrittsvortrag: Transformation graphischer Protokollspezifikationen in Model-Checker-AnfragenO4.267
07.11.2013Galina BesovaGrammar-based Model TransformationsO4.267
31.10.2013Oleg TravkinSPIN as a linearizability checker under weak memory modelsO4.267
24.10.2013Dominik SteenkenSMT Solving for Embedding Feasibility in Lazy State Space Construction for Abstract Graph TransformationO4.267
24.10.2013Tobias NickelAnalyse von Benutzeranforderungen von Service-Kompositionen mittels ModelcheckingO4.267
30.09.2013Matthias MulthauptGenerierung von Promela-Modellen aus Implementierungen von nebenläufigen Datenstrukturen in Form von LLVM IRO4.267
10.07.2013Sven WaltherKnowledge-based Verification of Service Compositions - an SMT ApproachO4.267
04-07.2013Dominik SteenkenPredicate Mining in Graph Traces via InterpolationO4.267
27.06.2013Oleg TravkinProgrammspezifikation für Linearisierbarkeitsbeweise unter schwachen SpeichermodellenO4.267
19.06.2013Alexander SchremmerTowards CEGAR of separation logic domains based on multi-parametric precisionsO4.267
06.06.2013Marie-Christine JakobsCertification for Configurable Program AnalysisO2.267
29.05.2013Michael FeldmannBachelor Thesis: Berechnung von Memory-Model-spezifischen KontrollflussgraphenO4.267
29.05.2013Tobias IsenbergBounded Model Checking of Graph Transformation Systems via SMT SolvingO4.267
22.05.2013Steffen ZiegertMultilevel Planning for Self-Optimizing Mechatronic SystemsO4.267
16.05.2013Sven WaltherGenerating Loop Invariants using TemplatesO4.267
15.05.2013Steffen BeringerAUTOSARO4.267
18.04.2013Tobias IsenbergInductive MethodsO4.267
21.03.2013Mike CzechDreiwertiges Model Checking paralleler Systeme mit heuristisch geleiteter Generierung von GegenbeispielenO3.267
11.03.2013Nikolaos IkonomakisCombining Three-Valued Logic and Quantified Boolean Formulae in Bounded Model Checking EncodingsO4.267
07.02.2013Steffen ZiegertDurative Graph Transformations: Semantics and PropertiesO2.267
29.01.2013Thomas HauckMultiagenten-Koordination in temporaler PlanungO3.267
29.01.2013Alexander SchremmerSeparation Logic meets CEGARO3.267
28.01.2013Marcel FriedrichSuchraumeinschränkung für Graphgrammatiken durch temporallogische FormelnO2.267
23.01.2013Antonio AttimonelliEin Tool zur automatischen Generierung von GraphabstraktionenO4.267
10.01.2013Oleg TravkinTowards Memory-Model-aware Semantics for High Level LanguagesO3.267
20.12.2012Sven WaltherA Primer on Description LogicsO3.267
19.12.2012Shayan AhmadianExploiting Planning Graphs and Landmarks for Efficient GTS PlanningO4.267
13.12.2012Dominik Steenken
Manuel Töws
Counterexample Analysis via Shape Constraints
Abstraction Maintenance and Counterexample Analysis in SGA
O3.267
29.11.2012Annika Mütze
Maryam Sanati
Memory Model-Aware Model Checking 
A Library of Platform Models for Model Weaving and Verification
O3.267
22.11.2012Galina BesovaGeneric and Domain Specific Method EngineeringO4.267
08.11.2012Nils TimmHeuristic-Guided Abstraction Refinement for Concurrent SystemsO4.267
18.10.2012Tobias IsenbergBounded Model Checking für Graphtransformationssysteme als SMT-ProblemO4.267
26.09.2012Galina BesovaWeaving-Based Configuration and Modular Transformation of Multi-Layer SystemsO4.267
25.07.2012Steffen ZiegertApproaches to Cooperative PathfindingO4.267
11.07.2012Sven WaltherGeneric Reasoning about Specific DomainsO4.267
28.06.2012Nils TimmHeuristic-Guided Abstraction Refinement for Concurrent SystemsO4.267
11.06.2012Oleg TravkinLinearisierbarkeit anhand lokaler Beweisverpflichtungen - Fallstudie: MultisetO4.267
04.06.2012Alexander SchremmerAbstraction Refinement in UFOO4.267
10.05.2012Dominik SteenkenEin Konzept für eine vollautomatische Erreichbarkeitsanalyse für Shape GraphenO4.267
03.05.2012Thomas RuhrothModeling and Verification of Secure Information Flow Properties in UMLsec- ModelsO4.267
12.04.2012Galina BesovaModel-driven Development of Model Transformations O4.267
01.02.2012Daniel WonischProof Simplification by Program TransformationO4.216
26.01.2012Sven WaltherAvoiding State Space Explosion using Pairwise CompositionO4.216
12.01.2012Steffen ZiegertPerspectives in Planning with Graph TransformationO4.216
08.12.2011Nils Timm3-valued Abstraction for (Bounded) Model CheckingO4.216
01.12.2011Oleg TravkinMulti-Core Memory Models - Eine EinführungO4.216
17.11.2011Alexander SchremmerRuntime VerificationO4.216
27.10.2011Dominik SteenkenWord Level Bitvector Interpolation for VerificationO4.216

Die Universität der Informationsgesellschaft