ABSTRACT. Naval systems are becoming more and more complex as they are increasingly integrated with a significant increase in software parts. The complexity also comes from many modes in systems ranging from complete automation to secondary modes requiring the intervention of human operators. Validation naval systems must take into account all these aspects which are no longer manageable without the assistance of computer tools. This presentation will present examples of naval systems as well as properties to verify, for which real failures have been observed and for which the use of formal methods is necessary. A focus on performance properties and software validation will be realized during this presentation. The purpose of this presentation is to stimulate discussions between the industrial needs of formal validation in naval systems and the current academic solutions that could address these issues.

ABSTRACT. The complexity of modern aircraft development is rising constantly pushed by the growth of the transportation market, the continuous technology improvements, the rising of new technologies, the development of more challenging regulations and the ever increasing competition. The high cost investments involved with the development of an aircraft and its constituent systems leads airframers and system suppliers to take critical design decisions early, with a potentially high risk on the development and operational costs of the aircraft. On the other hand, the increasing complexity makes the costs and risks connected with the verification and testing of aircraft systems and their integration constantly rising.

These considerations are pushing the aerospace industry towards growing deployment of model-based methods to anticipate design problems closer in time to when the design decisions are taken, to reduce the risk of turn-backs and migrate towards a virtual testing driven development process to gradually achieve right-the-first-time test rig campaigns and safety-of-flight.

In this evolving landscape, promising model-based technologies beyond simulation are emerging to support this view, including property falsification, automatic test generation and coverage and formal verification technologies. Nonetheless, there still remain compelling challenges to overcome to render these technologies widely applicable across the aerospace industry. In this paper, we present such challenges and position them in context of the development process of aerospace systems and relevant aerospace engineering standards.

ABSTRACT. We present a compositional validated integration method based on Taylor models.

Our method combines solutions for lower dimensional subsystems into solutions

for a higher dimensional composite system, rather than attempting to solve the

higher dimensional system directly. We have implemented the method in an

extension of the Flow* tool. Our preliminary results are promising, suggesting

significant gains for some biological systems with nontrivial compositional

structure.

ABSTRACT. With the increasing power of computers, real-time algorithms tends to become more complex and therefore require better guarantees

of safety. Among algorithms sustaining autonomous embedded systems, model predictive control (MPC) is now used to compute

online trajectories, for example in the SpaceX rocket landing. The core components of these algorithms, such as the convex

optimization function, will then have to be certified at some point. This paper focuses specifically on that problem and presents

a method to formally prove a primal linear programming implementation.

We explain how to write and annotate the code with Hoare triples in a way that eases their automatic proof. The proof process

itself is performed with the WP-plugin of Frama-C and only relies on SMT solvers.

Combined with a framework producing all together both the embedded code and its annotations, this work would permit to certify

advanced autonomous functions relying on online optimization.

ABSTRACT. In the past several years, syntax-guided synthesis (SyGuS) solvers have made significant progress as efficient backend reasoners in several applications. One approach for syntax-guided synthesis, as implemented in the SMT solver CVC4, has shown that SMT solvers can act as efficient stand-alone tools for synthesis. This talk focuses on a new enumerative approach for invariant synthesis in the SMT solver CVC4. We describe a divide-and-conquer approach that makes use of an evolving set of refinement lemmas that constrain concrete points of the invariant-to-synthesize. We show its applicability to synthesis in multiple SMT domains, including for synthesizing invariants that involve non-linear arithmetic.

ABSTRACT. Reachability analysis techniques are at the core of the current state-of-the-art technology for verifying safety properties of cyber-physical systems (CPS). In this talk, I will present a suite of parallel state-space exploration

algorithms in the tool XSpeed that, leveraging multi-core CPUs, enable to improve the performance of reachability

analysis of linear continuous and hybrid automaton models of CPS. A performance evaluation on several benchmarks

comparing their key performance indicators will be shown. This enables to identify the ideal algorithm and the

parameters to choose that would maximize the performances for a given benchmark.

ABSTRACT. The article highlights the closed link between the policy iterations algorithm and the Newton method.

The main different between them comes from the very special differential operator used for policy iterations

algorithm. We show that the policy iterations algorithm is sub-optimal in the sense that it does not fully exploit

the information provided by this special differential. Finally, we propose correlations between the hypothesis

that ensure the convergence of the algorithms.