ABSTRACT. Hybrid systems are systems with mixed discrete-continuous behavior. Despite intensive research during the last decades to offer algorithms and tools for the reachability analysis of hybrid systems, the available technologies still suffer from scalability problems. Though scalability can be increased on the cost of precision, it is not easy to find the right balance that leads to successful verification in acceptable time. In this talk we give a general introduction to hybrid systems and methods for their reachability analysis, introduce our HyPro tool, and report on some recent work to speed up the computations while still maintaining sufficient precision.

ABSTRACT. Modern cyber-physical systems (CPS) operate in complex systems of systems that must seamlessly work together to control safety- or mission-critical functions. Capturing specifications in LTL enables verification and validation of CPS requirements, yet an LTL formula specification can imply unrealistic assumptions, such as that all of traces populating the variables in the formula are of type Boolean and agree on a standard time step. To achieve formal verification of CPS systems of systems, we need to write validate-able requirements that reason over (sub-)system traces of different types, such as traces from different timescales, levels of abstraction, or traces with complex relationships to each other that populate variables in the same formula. Validation includes both transparency for human validation and tractability for automated validation, e.g., since CPS often run on resource-limited embedded systems. Specifications for correctness of numerical algorithms for CPS need to be able to describe global properties with precise representations of local components. Therefore, we introduce Mission-time Linear Temporal Logic Multi-Type (MLTLM), a logic building on MLTL, to enable writing clear, formal requirements over finite traces (e.g., sensor signals, local computations) of different types, cleanly coordinating the temporal logic and trace relationship considerations without significantly increasing the complexity of logical analysis, e.g., model checking, satisfiability, runtime verification. We explore the common scenario of CPS systems of systems operating over different timescales, including a detailed analysis with a publicly-available implementation of MLTLM.

ABSTRACT. Reinforcement learning (RL) is a popular technique in the AI and robotics domains to obtain control policies for autonomous agents operating in uncertain environments. The basic setup of RL is as follows: in any given state, the autonomous agent takes an action, and the environment stochastically decides the next state for the agent and also gives it a reward. Rewards are defined locally, and are associated with the agent transitions or states. RL algorithms attempt to find control policies that maximize the cumulative reward obtained by the agent. Recent work in these domains has focused on model-free RL, where a further challenge is that the model of the environment is unknown. A crucial element of RL is reward design: ill-designed rewards can make the agents learn undesirable or unsafe control policies – unacceptable in safety-critical systems. In the formal methods community, techniques like reactive synthesis have focused on correct-by-construction design of control policies given a model of the environment and formal specifications in a suitable temporal logic. In this talk, we will look at some recent work on how we can leverage powerful specification formalisms with model-free learning-based methods to get control policies that are safer, and in some cases, accompanied with safety guarantees.

ABSTRACT. Ordinary differential equations (ODEs) are used to model the evolution of the state of a system over time. They are ubiquitous in the physical sciences and are often used in computational models with safety-critical applications. For critical computations, numerical solvers for ODEs that provide useful guarantees of their accuracy and correctness are required, but do not always exist in practice. In this work, we demonstrate how to use the Coq proof assistant to verify that a C program correctly and accurately finds the solution to an ODE initial value problem (IVP). Our verification framework is modular, and concisely disentangles the high-level mathematical properties expected of the system being modeled from the low-level behavior of a particular C program. Our approach relies on the construction of two simple functional models in Coq: a floating-point valued functional model for analyzing the intermediate-level behavior of the program, and a real-valued functional model for analyzing the high-level mathematical properties of the system being modeled by the IVP. Our final result is a proof that the floating-point solution returned by the C program is an accurate solution to the IVP, with a good quantitative bound. Our framework assumes only the operational semantics of C and of IEEE-754 floating point arithmetic.

ABSTRACT. Motion planning algorithms are a vital part of autonomous robots that — simply put — turn tasks and constraints into sequences of motions that the robot shall follow. In its most basic form, motion planning asks how to reach a destination while avoiding obstacles. In this talk, we discuss motion planning allowing for more sophisticated tasks, constraints and preferences. We will discuss how to express these in temporal logics, and integrated with sampling-based motion planning algorithms. We will specifically focus on using Signal Temporal Logic (STL) as a powerful specification language with quantitative semantics and discuss what provable guarantees the planning algorithms can provide. Throughout the talk, we will showcase robotics applications, such as autonomous driving and exploration of unknown environments with UAVs.

ABSTRACT. Neural networks can be costly in terms of memory and execution time. Reducing their cost has become an objective, especially when integrated in an embedded system with limited resources. A possible solution consists in reducing the precision of their neurons parameters. In this article, we present how to use auto-tuning on neural networks to lower their precision while keeping an accurate output. To do so, we use a floating-point auto-tuning tool on different kinds of neural networks. We show that, to some extent, we can lower the precision of several neural network parameters without compromising the accuracy requirement.

ABSTRACT. In this presentation, we first introduce an adversarial test generation (falsification) framework for control systems with Neural Networks (NN) in the loop based on optimal control theory. We experimentally demonstrate that our framework outperforms black-box system testing methods. Then, we present a new approach for the NN repair problem. Given a set of adversarial samples, the NN repair problem seeks to modify the weights of the NN so that the adversarial samples are removed. We formulate and solve the NN repair problem as a Mixed Integer Quadratic Program (MIQP) that adjusts the weights of a single layer subject to the given safety constraints. We demonstrate the application of our framework on control problems.