FMAS 2025, Paris

Integrated Formal Methods for the Verification of Cyber-Physical and Autonomous Systems by Prof. Paula Herber

Abstract: Cyber-physical systems pose significant challenges for formal methods, due to their inherent heterogeneity and interaction with a physical environment. In addition, we see a tremendous increase in the use of learning to make autonomous decisions in dynamic environments, and an increasing demand to cope with uncertainties and unforeseen events. These developments call for the development of new theories and tools, but also for the integration of existing formal methods. In this talk, I will summarize some of our recent efforts towards developing methods for the integration of formal methods to support reusable specification and scalable verification of cyber-physical and autonomous systems.

Logic of Autonomous Dynamical Systems by Prof. Dr. André Platzer

Abstract: This talk highlights some of the most fascinating aspects of the logic of dynamical systems which constitute the foundation for developing cyber-physical systems (CPS) such as robots, cars and aircraft with the mathematical rigor that their safety-critical nature demands. Differential dynamic logic (dL) provides an integrated specification and verification language for dynamical systems, such as hybrid systems that combine discrete transitions and continuous evolution along differential equations. In dL, properties of the global behavior of a dynamical system can be analyzed solely from the logic of their local change without having to solve the dynamics. In addition to providing a strong theoretical foundation for CPS, differential dynamic logics as implemented in the KeYmaera X prover have been instrumental in verifying many applications, including the Federal Aviation Administration’s Airborne Collision Avoidance System ACAS X, a train control system for the Federal Railroad Administration, automotive systems, mobile robot navigation, and a surgical robot system for skull-base surgery. dL is the foundation to provable safety transfer from models to CPS implementations and is also the key ingredient behind autonomous dynamical systems for Safe AI in CPS.

FMAS 2024, Manchester

Self-Adaptation in Autonomous Systems by Dr Silvia Lizeth Tapia Tarifa

Abstract: Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. A self-adaptive system (SAS) can be realised as a multi-layered system, e.g., a two-layered systems that have a separation of concerns between the domain-specific functionalities of the system (the managed subsystem) and the adaptation logic (the managing subsystem), which introduces an external feedback loop for managing adaptation in the system; or as a three-layered system, where the third layer can implement a feedback loop for architectural self-adaptation, which is used to reconfigure the second layer (the adaptation logic of the managing subsystem). In this talk I will present techniques that can capture the SAS’s variability, concretely software product lines, where the managing subsystem of an SAS can be modelled as a control layer capable of dynamically switching between valid configurations of the managed subsystem; and declarative stages in a lifecycle of a system, where we do not require explicit modelling of the transitions between stages in the lifecycles of a system; however, characteristics on an stage can be observed, which after observation may trigger changes in the self-adaptation logic itself.

Proof for Industrial Systems using Neural Certificates by Prof. Daniel Kröning

Abstract: We introduce a novel approach to model checking software and hardware that combines machine learning and symbolic reasoning by using neural networks as formal proof certificates. We train our neural certificates from randomly generated executions of the system and we then symbolically check their validity which, upon the affirmative answer, establishes that the system provably satisfies the specification. We leverage the expressive power of neural networks to represent proof certificates and the fact that checking a certificate is much simpler than finding one. As a result, our machine learning procedure is entirely unsupervised, formally sound, and practically effective. We implemented a prototype and compared the performance of our method with the state-of-the-art academic and commercial model checkers on a set of Java programs and hardware designs written in SystemVerilog.

FMAS 2023, Leiden

Formal methods within the TAS Governance node by Prof. Alice Miller

Abstract: The TAS Governance Node part of the £33M Trustworthy Autonomous Systems Programme funded by the UKRI Strategic Priorities Fund. The aim of the node is to explore how to make autonomous systems aware of — and responsive to — changing regulations. Led by the University of Edinburgh, it brings together researchers from the universities of Edinburgh, Glasgow, Nottingham, Heriot-Watt, Sussex, and Kings College London; as well as multiple industrial partners. In this talk I will highlight some of the activities within the node, focussing on those that use Formal Methods. These include:

  • an automatic theory repair system for a legal responsibility framework for autonomous vehicles,
  • accident anticipation through reasoned simulation,
  • robot planning using in-situ model checking; and,
  • (formal aspects of) a node-wide automotive case study investigation.

SMT: Something you Must Try [Joint talk with iFM] by Prof. Erika Ábrahám

Abstract: SMT (Satisfiability Modulo Theories) solving is a technology for the fully automated solution of logical formulas. Due to their impressive efficiency, SMT solvers are nowadays frequently used in a wide variety of applications. These tools are general purpose and as off-the-shelf solvers, their usage is truly integrated. A typical application encodes real-world problems as logical formulas, whose solutions can be decoded to solutions of the real-world problem.

In this talk we give some insights into the mechanisms of SMT solving, discuss some areas of application, and present a novel application from the domain of simulation.

FMAS 2022, Berlin

Common Ground in Moral Norms by Marija Slavkovik

Abstract: Any ethically behaving autonomous system needs a specification of what the right and wrong thing to do is. Who decides what right and wrong is for a machine? In the absence of a moral theory that can be neatly translated into an algorithm (and machines that have high level of situational awareness), the specification of what is right and wrong is likely to come as a rule-of-thumb: dynamic, context specific and sourced from various stakeholders. These moral norms are likely to be conflicting. We explore: What is a common ground in a set of conflicting norms? How do we approach moral norm conflicts and build algorithms that resolve them?

Her talk is based on a recent paper, available at https://arxiv.org/abs/2209.06455

Formal Verification for Neural Networks in Autonomous Cyber-Physical Systems by Taylor T. Johnson

Abstract: The ongoing renaissance in artificial intelligence (AI) has led to the advent of data-driven machine learning (ML) methods deployed within components for sensing, actuation, and control in safety-critical cyber-physical systems (CPS). While such learning-enabled components (LECs) are enabling autonomy in systems like autonomous vehicles, robots, and other autonomous CPS, as demonstrated in part through recent accidents in semi-autonomous/autonomous CPS and by adversarial ML attacks, ensuring such components operate reliably in all scenarios is extraordinarily challenging. We will discuss formal methods for assuring specifications—mostly robustness and safety—in autonomous CPS using our software tools NNV (Neural Network Verification: https://github.com/verivital/nnv) and Veritex (https://github.com/verivital/veritex ), developed as part of an ongoing DARPA Assured Autonomy project. These tools have been evaluated in CPS development with multiple industry partners in automotive, aerospace, and robotics domains, and allow for analyzing neural networks and their usage in closed-loop systems. We will briefly discuss relevant ongoing community activities we help organize, such as the Verification of Neural Networks Competition (VNN-COMP) held with CAV the past few years, as well as the AI and Neural Network Control Systems (AINNCS) category of the hybrid systems verification competition (ARCH-COMP). We will conclude with a discussion of future directions in the broader safe and trustworthy AI domain, such as in new projects verifying neural networks used in medical imaging analysis.

FMAS 2021, Online

Help or Hazard: Towards Verifying Autonomous Robot Systems by Clare Dixon

Abstract: Autonomous robotic systems are being developed to operate in a range of environments: industrial, transport, healthcare and domestic and have the potential to be of great benefit to society. Further, they may be assisting, collaborating with or working near humans. We must make sure they are safe, robust, reliable and trustworthy and they themselves don’t become become the hazard. In this talk I will discuss ways to verify such systems, relating to research carried out over a number of projects with different types of robot, operating in a range of scenarios.

Understanding and Verifying Deep Neural Networks by Divya Gopinath

Abstract: Deep Neural Networks (DNNs) have gained immense popularity in recent times and have widespread use in applications such as image classification, sentiment analysis, speech recognition and also in safety-critical applications such as autonomous driving. However, they suffer limitations such as lack of explainability and robustness which raise safety and security concerns in their usage. Further, the complex structure and large input spaces of DNNs act as an impediment to thorough verification and testing. The SafeDNN project at the Robust Software Engineering (RSE) group at NASA aims at exploring techniques to ensure that systems that use deep neural networks are safe, robust and interpretable. In this talk, I will be presenting our technique Prophecy that automatically infers formal properties of deep neural network models. The tool extracts patterns based on neuron activations as preconditions that imply certain desirable output properties of the model. I would be highlighting case studies that use Prophecy in obtaining explanations for network decisions, understanding correct and incorrect behavior, providing formal guarantees wrt safety and robustness, and debugging neural network models. We have applied the tool on image classification networks, neural network controllers providing turn advisories in unmanned aircrafts, regression models used for autonomous center-line tracking in aircrafts and neural network object detectors.