Luca Brodo
Portrait of Luca Brodo

Luca Brodo

Formal Methods & Software Engineering
Hamm-Lippstadt University of Applied Sciences

I work on making formal verification of software-intensive and cyber-physical systems cheaper to apply and easier to keep correct as systems evolve. My research covers property refinement for temporal-logic specifications, timed refinement for safe post-deployment updates of real-time systems, and verifiable self-adaptation for autonomous systems. I am supervised by Stefan Henkler.

Research

Property refinement and specification debt

Temporal-logic specifications accumulate redundant properties over design iterations. I develop property refinement for LTL and CTL to identify properties that are already implied by others and to reduce verification to a minimal sufficient set.

Timed refinement for evolving real-time systems

Updates to deployed real-time systems must preserve what was verified before. Relaxed Weak Timed Bisimulation (RWTBS) checks such updates compositionally, preserving output timing strictly while relaxing input timing in a controlled way.

Self-adaptive and socially compliant autonomous systems

Autonomous systems must adapt at runtime and behave acceptably around people. I study runtime self-optimization with exact optimality guarantees and the verification of social norms alongside safety and liveness.

More on my research

Selected publications

  1. Asymmetric Timed Refinement for Correct Post-Deployment Updates in Real-Time Systems

    Luca Brodo, Giuseppe Scalora, Stefan Henkler

    MEMOCODE 2026AcceptedBest Paper Award

    Introduces Relaxed Weak Timed Bisimulation (RWTBS), a refinement relation for real-time systems that strictly preserves output timing while allowing controlled relaxation of input reception timing, so buffered or asynchronous updates can be validated compositionally.

  2. Property Refinement in Linear Temporal Logic: Formal Semantics and Algorithms for Software Verification

    Luca Brodo, Giuseppe Scalora, Stefan Henkler

    FSE 2026

    Formal theory and algorithm for finding LTL properties that are already implied by stronger ones, so a verification suite can be reduced to a minimal sufficient set before model checking.

  3. Runtime Self-Optimization Through Knowledge-Driven Design Space Reduction

    Luca Brodo, Giuseppe Scalora, Stefan Henkler

    SEAMS 2026

    Lets cyber-physical systems re-optimize their configuration at runtime by caching proven-optimal solutions as zonotope regions and pruning the design space, keeping exact optimality with heuristic-level speed.

All publications

Contact

luca.brodo@hshl.de
Hamm-Lippstadt University of Applied Sciences, Campus Lippstadt
Dr.-Arnold-Hueck-Straße 3, 59557 Lippstadt, Germany