Luca Brodo

Publications

Each title links to a page with the full abstract, a summary and a BibTeX entry. You can also find my publications on Google Scholar and ORCID.

Selected

  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.

2026

  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. Correct-by-Construction Evolution of Digital Twins for Real-Time Autonomous Systems

    Luca Brodo, Giuseppe Scalora, Stefan Henkler

    ASYDE 2026 Workshop

    Uses refinement twice in digital-twin–based engineering: to guarantee that updates proposed by a digital twin preserve certified behaviour (via RWTBS), and to generate FreeRTOS and ROS 2 code from timed automata that is correct by construction.

  3. Bridging Social and Technical Compliance in Autonomous Systems through a Standardized Pattern Catalog

    Luca Brodo, Giuseppe Scalora, Lukas Walter, Stefan Henkler

    MODELS 2026 Companion

    A catalog of reusable observer patterns for regulative and constitutive social norms, each with a natural-language template, a (T)CTL formalization and an observer automaton for model checking.

  4. Property Refinement in Computation Tree Logic

    Luca Brodo, Giuseppe Scalora, Stefan Henkler

    CAIESA 2026 Workshop

    Closes the gap left by simulation-based CTL refinement: a complete, decidable refinement theory and an exact algorithm, evaluated on more than 3,000 suites with over 52,000 properties.

  5. 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.

  6. 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.

  7. What Do We Really Need? Identifying Minimal Sufficient Temporal Properties via Refinement

    Luca Brodo, Giuseppe Scalora, Stefan Henkler

    ICSE 2026 Companion

    A refinement relation for CTL properties, based on trace inclusion with a non-emptiness guard, that identifies which properties of a specification suite are already guaranteed by others.

2025

  1. Towards a Digital Twin Framework for Secure and Efficient Cyber-Physical Transportation Systems

    Luca Brodo, Giuseppe Scalora, Stefan Henkler

    MoVe4SPS 2025 Workshop

    A digital twin framework for a centralised network of autonomous vehicles carrying people and goods, combining model predictive control for efficiency with behavioural profiling for intrusion detection.