Latest News

The 2024 ConVeY Spring Workshop took place on April 6, 2024 in Luxembourg, collocated with ETAPS 2024. Thank you to all participants for the interesting talks and discussions.

Overview

Networks, computers, sensors, and actuators are being increasingly integrated into cyber-physical systems, i.e., software systems that interact with the physical world and must cope with its continuous behavior. An increasing number of cyber-physical systems operate in safety-critical domains, e.g., autonomous vehicles, robotic surgery, traffic control, human-robot collaboration, and smart grids. For this reason, their design and deployment should ideally be accompanied by a formal check of correct behavior. A fundamental challenge in the verification of cyber-physical systems is the fact that they are subject to change. The physical environment changes continuously, at runtime, and in ways that cannot be completely foreseen at the design stage. At the same time, the requirements may change. Sought-after aspects include more functionality, lower power consumption, or faster response. In many cases, the system should be migrated to a different hardware platform. To face this multi-level continuous change, we propose to

1. develop verification and synthesis technology for robust system design, i.e., for the design of systems that maintain correct behavior under change
2. develop verification and synthesis technology able to cope with frequent or even continuous change in the specification and the environment.

Areas of Research

Robust System Design

We will develop techniques to guarantee correct behavior under changes in plant parameters, under certain classes of perturbations including sensor measurement errors, and under uncertainties introduced by the implementation platform. In particular, we will investigate the design of controllers that are robust by construction against those changes.

Evolving Systems

Novel construction and verification techniques shall be investigated that adapt to offline changes in the specification, the hardware, or the implementation of control software, and reuse efforts from earlier stages as much as possible.

On-the-fly Synthesis and Verification

We will develop techniques for the online verification and synthesis of controllers that operate—and provide a correctness guarantee—only within a given time horizon. Repeated execution of this procedure, combined with availability of a fail-safe strategy, ensures safe operation.

Open Positions

ConVeY seeks excellent PhD students. The next batch of students starts on July 1, 2024. Application deadline is April 21.