ABSTRACT. Automotive systems, such as Scania trucks, are complex collections of software and hardware. A typical Scania truck has tens of Electronic Control Units (ECUs), with each ECU having one or more application modules—embedded software that interacts with and controls physical actuators and sensors. Scania trucks and their ECUs must adhere to rigorous requirements on functionality, safety, and security. Standards such as ISO 26262 provide general system-level requirements on safety and security, while ECU and application module requirements are company-internal individual documents in structured natural language. This is complemented by general coding standards for common module implementation languages, such as MISRA-C for C modules. For the last ten years, we have conducted research aimed at enabling automotive systems, such as Scania trucks and their ECUs, to demonstrably meet their requirements through formal reasoning. We have considered both sound decomposition of system level requirements, e.g., on braking, and lower-level formal specification and verification of application module C code. This extended abstract presents an overview of what we believe are the current key problems in achieving trustworthy automotive systems, based on our experience from case studies involving ECU software modules and their requirements in Scania trucks. Finally, we give an outlook on directions and next steps.

ABSTRACT. CoSApp, for Collaborative System Approach, is a Python library dedicated to the simulation and design of multi-disciplinary systems. It is primarily intended for engineers and system architects during the early stage of industrial product design. The API of CoSApp is focused on simplicity and explicit declaration of design problems. A very flexible mechanism of solver assembly allows users to construct complex, customized simulation workflows. This presentation focuses on a key feature of the framework, namely the simulation of multimode systems with event-driven mode transitions. This feature allows one to model systems that undergo discontinuities (contact problems, threashold effects, etc.), as well as possible dynamic reconfigurations. We will discuss the challenges of designing such systems, through real-life industrial examples.

ABSTRACT. The ∆Q Systems Development paradigm (∆QSD) is a novel industrially-derived systems development methodology for developing complex real-world distributed systems that directly employs statistical performance metrics from the outset of the system design process and throughout the entire software production life cycle. It uses a stochastic approach to specify system behaviour, using cumulative distribution functions to model both delay and failure together. Experience shows that this is a ‘sweet spot’ that gives good results with little computation requirements. Predictions are accurate when the system model correctly captures both independent and dependent parts. This paradigm has been developed by the Welsh company PNSol over a period of 20+ years, in collaboration with IOG (formerly IOHK), BT, Vodafone, Boeing, Space and Defence, as well as other major companies who focus on the development of reliable high-quality, high integrity, distributed software systems, with strong real-time requirements. This talk will be a brief ∆QSD overview with an emphasis on compositionality, lightweight formal semantics, and the ∆QSD challenges in systems engineering.

ABSTRACT. We present a runtime-monitoring framework for vision-based autonomous systems in which a single trained encoder predicts a \emph{semantic basis} of past-time signal-temporal-logic (ptSTL) atoms, and any specification in a fixed fragment is then evaluated by a deterministic, monotone, $1$-Lipschitz decoder derived from the formula's parse tree. The compositional algebraic structure of the decoder lets a single conformal calibration pass certify the entire fragment simultaneously, with no per-formula retraining and no union bound over specifications. We prove that within monotone, $1$-Lipschitz reusable interfaces the semantic basis is the minimum sufficient prediction target. We also introduce a \emph{rolling} architecture that calibrates before temporal aggregation, trading certified tightness at long horizons for an easier per-step learning problem. On a pedestrian-crossroad benchmark and on real-world Waymo driving data, the two architectures cover complementary horizon regimes and decisively outperform a Bonferroni-corrected observer baseline.

ABSTRACT. We present an integrated framework that unifies runtime verification and model-based diagnosis within the stream specification language LOLA. By encoding system descriptions, component health states, and observations into a single stream-based formalism, the approach enables continuous, online fault localization directly alongside fault detection, without requiring separate toolchains. The framework supports both time-invariant and transient faults, and naturally accommodates nondeterministic observations.

ABSTRACT. The 2015 GEO-CAPE ROIC In-Flight Performance Experiment (GRIFEX) is a long-duration CubeSat whose telemetry began exhibiting recurring off-nominal behavior in 2020, late in the mission, motivating verification methods that can support both design-time reasoning and deployable runtime monitoring. Pacti is attractive for this setting because it performs compositional analysis over assume-guarantee contracts, but temporal behavior in Pacti is expressed only indirectly by stitching together scenarios. Mission-time Linear Temporal Logic (MLTL) provides the bounded temporal expressivity needed to state progression and recovery requirements directly, while R2U2 provides a realizable runtime-monitoring backend. We present BB-AGT, a bounded-behavior assume-guarantee translator that lifts named Pacti contracts into bounded future-time MLTL formulas, equips them with predicates such as active, holds, and viol, and lowers the result into machine-generated C2PO monitor specifications for R2U2. We evaluate this translation on a contract model of GRIFEX; on Pacti's Mars entry, descent, and landing scenario; and on a smaller habitat design example. In the GRIFEX study, the resulting model synthesizes one monitor set from 287 contracts and 275 formulas. In the Mars EDL study, BB-AGT turns an allocation-oriented contract model into 9 explicit bounded monitoring formulas and matching runtime monitors.

ABSTRACT. Synergic modeling is a paradigm in which system identity is grounded in coherence constraints over admissible trajectory spaces rather than in state transitions. A coherence constraint C=(φ, ψ) pairs a pointwise predicate φ that excludes instantaneously incoherent crossviewpoint state combinations with a trajectory predicate ψ that bounds their temporal evolution. Instantiated on an adaptive drone, we derive a catalogue of 20 LTL properties verified exhaustively in nuXmv, and show how the same C translates directly into a lightweight runtime monitor embedded in a MAPE-K loop. We claim a design/monitoring duality: a coherence constraint functions as a proof obligation at design time and as an observation specification at runtime, thus connecting formal verification and runtime assurance through a single compositional contract.

ABSTRACT. Autonomous robotic systems are increasingly being developed for safety-critical environments, where ensuring safe operation is essential. Robots are typically implemented using modular software frameworks, each with its own distinct requirements and verification artefacts. We are interested in a bottom-up, compositional approach to their specification using Assume Guarantee (AG) contracts in which the specifications of the individual modules are used to compute a system-wide property. In this ongoing work, we extend an existing compositional framework by incorporating a more expressive temporal logic (MTL) as the foundation of the top-level specification language and developing a corresponding calculus for node composition. We demonstrate one of the rules for node composition using an illustrative example and discuss the planned future extensions to this framework.

ABSTRACT. Full verification of learning-enabled cyber-physical systems (CPS) has long been intractable due to challenges including black-box components and complex real-world environments. Existing tools either provide formal guarantees for limited types of systems or test the system as a monolith, but no general framework exists for compositional analysis of learning-enabled CPS using varied verification techniques over complex real-world environments. This paper introduces a verification theory and framework that aims to fill this gap, enabling the construction of sound, formally-checked assurance cases for CPS. Our framework supports: (1) environment modeling using the Scenic probabilistic programming language; (2) compositional system modeling with clear component interfaces, ranging from interpretable code to black boxes; (3) assume-guarantee contracts over those components using an extension of Linear Temporal Logic containing arbitrary Scenic expressions; (4) evidence generation through testing, formal proofs in proof assistants, and external assumptions; (5) sound combination of generated evidence using contract operators; and (6) automatic generation of assurance cases tracking the provenance of system-level guarantees. We implement our framework in a tool, ScenicProver, using Pacti and Lean 4 as contract/proof backends. We demonstrate its effectiveness through a case study on an automatic emergency braking system with sensor fusion. By leveraging manufacturer guarantees for sensors and focusing testing effort on uncertain conditions, our approach enables stronger probabilistic guarantees than monolithic testing with the same computational budget.

ABSTRACT. LLM coding assistants now generate substantial bodies of systems code in C and Rust (kernels, compilers, drivers) that arrive without specifica- tions and with safety contracts encoded implicitly at call sites rather than enforced at function boundaries. We propose agentic model checking, a ver- ification paradigm coupling LLM agents with a bounded model checking backend under the principle agents propose, solvers verify. Agents handle every task requiring semantic judgment (specification inference, check se- lection, counterexample classification, refinement proposal); a BMC back- end (CBMC for C, Kani for Rust) discharges every soundness-relevant de- cision. Verification is compositional at function granularity under assume- guarantee contracts, and refinements propagate across the call graph. We instantiate the paradigm in BMC-Agent and evaluate it on LLM-generated kernel and compiler code in both languages and on five OSS-Fuzz-hardened libraries.

ABSTRACT. Exploring cyber-physical system (CPS) architectures that satisfy a set of heterogeneous requirements while minimizing a cost metric is computationally challenging, due to the exponential growth of the design space with the number of architecture parameters and to the interdependencies between architectural choices and system properties. We present architecture exploration methodologies that leverage assumeguarantee (A/G) contracts for decomposition at every stage of the exploration pipeline: specification (via viewpoint and satisfiability modulo convex programming (SMC) contracts), synthesis (via mixed integer linear programming (MILP) or binary integer programming (BIP)), verification (via refinement and convex programming (CP) checks), and pruning (via subgraph isomorphism and certificates from irreducible infeasible sets (IISs) and counterexamples). Experiments on a reconfigurable production line and an aircraft electrical power distribution network show one to two orders of magnitude acceleration over comparable approaches, enabling tractable design on instances where prior methods time out.

ABSTRACT. Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. In this talk, we present Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct program logics in a modular and compositional way. HDL mirrors the architecture of satisfiability modulo theories (SMT): Individual dynamic logics, along with their proof calculi, are treated as dynamic theories that can be combined to reason about heterogeneous systems whose components are verified using different program logics. Combined theories allow program combination via regular programs, which yields heterogeneous control structures that allow us to reason about intertwined cross-language behavior.

ABSTRACT. This extended abstract summarizes recent results towards a computable and compositional semantics for hybrid systems.

ABSTRACT. Concurrency entails nondeterminism and interference: a program can have more than one possible run and the executions of different processes may conflict in unpredictable ways. A modular contract-based approach is essential for deductive verification to be manageable. However, specifying contracts for concurrent programs poses many challenges. Our approach to address these challenges for single-threaded cooperative scheduling is the following: 1) we specify concurrent behaviors with "context-aware trace contracts" (CATs for short) which allow the specification of internal non-functional behaviors of a procedure as well as the context of its execution; 2) we define a specification abstraction paradigm to reduce the specification effort and specify a single contract (Big CAT) for each procedure, rather than specifying each possible relevant scheduling choice; 3) we restrict program execution to "linear concurrency", i.e. concurrency without interleaving of tasks, to achieve modular verification at the granularity of procedure. We designed a sound deductive system to verify (Big) CATs for concurrent programs. We proved that program correctness entails the absence of interleaving and deadlock-freedom.

ABSTRACT. Complex engineered systems span hardware, software, control, planning, and operations. Their difficulty lies in coupling: a sensor changes the feasible estimator, a battery changes the feasible mission, and a planner changes which robot architecture is worth building. This presentation proposes monotone co-design as a formal, compositional language for these trade-offs. Starting from the classical functionality--resource interface, we explain how local feasibility relations compose, how Pareto queries avoid full Cartesian-product enumeration, how linear design problems yield scalable exact algorithms, and how distributional uncertainty and online learning extend the framework to risky, adaptive, and black-box subsystems. We close with applications in robotics, mobility, and heterogeneous multi-agent systems.