E-mail senden E-Mail Adresse kopieren
Forschungsgruppe

Jacobs

Rigorous Analysis and Design (RAD)

Die Forschungsgruppe Rigorous Analysis and Design (RAD) entwickelt grundlegende Techniken für die Analyse und den Entwurf von Systemen mit beweisbarer Korrektheitsgarantie. Dazu gehören Ansätze für die Analyse von Software im Hinblick auf Sicherheitseigenschaften und potenzielle Informationslecks sowie der automatische Entwurf beweisbar korrekter Systeme aus formalen Spezifikationen, d. h. die Programmsynthese. Eine unserer Hauptforschungsfragen ist, wie man die Analyse und den Entwurf von Systemen mit einer parametrischen Anzahl von Komponenten automatisieren kann, um Korrektheitsgarantien unabhängig von deren Größe zu erhalten.

Gruppenleiter:in

Swen Jacobs

E-Mail

Adresse

Kaiserstraße 21
66386 St. Ingbert (Germany)

Neueste Veröffentlichungen

Jahr 2022

Konferenz / Medium

FMCAD
FMCAD 2022Formal Methods in Computer-Aided Design 2022

Jahr 2021

Konferenz / Medium

CAV
Computer Aided Verification - 33nd International Conference, CAV 202133rd International Conference on Computer-Aided Verification

Jahr 2020

Konferenz / Medium

ATVA
Automated Technology for Verification and AnalysisAutomated Technology for Verification and Analysis

Konferenz / Medium

CAV
Computer Aided Verification - 32nd International ConferenceComputer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I

PROJECTS

This project aims at developing new methods and tools for the verification and synthesis of distributed and parameterized systems, such as communication protocols with a given or even a parametric number of components. To this end, we study approaches for the verification of distributed and parameterized systems and generalize the underlying ideas to develop novel methods for the more difficult task of automatic synthesis. This includes the development of efficient methods for the distributed synthesis problem with finite-state components, reductions from parameterized to distributed verification and synthesis, and methods for the synthesis of distributed infinite-state systems.

Further Information