Send email Copy Email Address
Research Group

Jacobs

Rigorous Analysis and Design (RAD)

The Rigorous Analysis and Design (RAD) group develops fundamental techniques for the analysis and design of systems with provable correctness guarantees. This includes approaches for the analysis of software with respect to safety properties and potential information leaks, as well as the automatic design of provably correct systems from formal specifications, i.e., program synthesis. One of our main research questions is how to automate the analysis and design of systems with a parametric number of components, in order to obtain correctness guarantees regardless of their size.

Head of Group

Swen Jacobs

Email

Address

Kaiserstraße 170-174
66386 St. Ingbert (Germany)

Most Recent Publications

Year 2021

Conference / Medium

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

Year 2020

Conference / 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

Year 2019

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