CISPA is currently in the founding process to join the German Helmholtz Association as a new member. It is consequently undergoing significant organizational changes, which are not yet reflected on this webpage.

For further information on the above mentioned founding process, please refer to the official press release by the State Chancellery of Saarland.

Recent News on the Transformation Process


The location of the first construction phase has been agreed upon. For further information, please refer to the official press release .

Resilient embedded systems


The resilient embedded systems research area explores the secure and dependable design and implementation of computing systems subject to stringent timing and resource constraints.

Real-time and embedded systems are virtually part of most modern technologies such as cars (e.g., engine control, anti-lock brakes, etc.), airplanes (e.g., fly-by-wire), or robotics (e.g., signal processing, actuator control). In such safety-critical domains, embedded real-time systems must be predictable, dependable and secure in the sense that correct outputs must always be produced at the right time, often under the presence of malicious actions. These requirements must be fulfiled on a tight resource budget, as embedded systems are commonly deployed in environments that impose severe space, weight, cost and power constraints.

Our research spans the entire range from the exploration of fundamental algorithmic issues to actual systems-building, and we particularly emphasize the intersection of both research approaches.


VatiCAN - Vetted, Authenticated CAN Bus

Deducing User Presence from Inter-Message Intervals in Home Automation Systems

Datenspeicherung in modernen Fahrzeugen – wem „gehören” die im Fahrzeug gespeicherten Daten?

Lightweight verification of separate compilation

A Survey on Static Cache Analysis for Real-Time Systems

A Tutorial on Human Activity Recognition Using Body-worn Inertial Sensors

Building timing predictable embedded systems

Blocking Optimality in Distributed Real-Time Locking Protocols

Basic Problems in Multi-View Modeling

Deductive control synthesis for alternating-time logics

Edit Distance for Timed Automata

Reverse engineering of cache replacement policies in Intel microprocessors and their evaluation

Extrapolation and Prediction of User Behaviour from Wireless Home Automation Communication

A Pipelined Multi-core MIPS Machine -- Hardware Implementation and Correctness Proof

Automatic Compositional Synthesis of Distributed Systems

Detecting Unrealizable Specifications of Distributed Systems

Fast DQBF refutation

JTACO: Test Execution for Faster Bounded Verification

Petri Games: Synthesis of Distributed Systems with Causal Memory

Security and Privacy Challenges in On-The-Fly Computing

A Fully Preemptive Multiprocessor Semaphore Protocol for Latency-Sensitive Real-Time Applications

An asymptotically optimal real-time locking protocol for clustered scheduling under suspension-aware analysis

Compositional Equivalence Checking for Models and Code of Control Systems

Efficient partitioning of sporadic real-time tasks with shared resources and spin locks

Improved analysis and evaluation of real-time semaphore protocols for P-FP scheduling

Multiprocessor Feasibility Analysis of Recurrent Task Systems with Specified Processor Affinities

Measurement-based modeling of the cache replacement policy

Precise timing analysis for direct-mapped caches

On Spin Locks in AUTOSAR: Blocking Analysis of FIFO, Unordered, and Priority-Ordered Spin Locks

Supervisor Synthesis for Controller Upgrades

Schedulability Analysis of the Linux Push and Pull Scheduler with Arbitrary Processor Affinities

The OMLP family of optimal multiprocessor real-time locking protocols

A Holistic View of Security and Privacy Issues in Smart Grids

FPGA-accelerated Key Search for Cold-Boot Attacks against AES

Privacy Enhanced Architecture for Smart Metering

Smart Grid and Method for Operating a Smart Grid

Dependability Results for Power Grids with Decentralized Stabilization Strategies

An Empirical Evaluation of the Influence of the Load-Store Unit on WCET Analysis

Completing the Automated Verification of a Small Hypervisor - Assembler Code Verification

Do not Snoop my Habits: Preserving Privacy in the Smart Grid

Homomorphic Primitives for a Privacy-Friendly Smart Metering Architecture

Model Checking Information Flow in Reactive Systems

Softer Smartcards: Usable Cryptographic Tokens with Secure Execution