Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models

This paper presents Fossil 2.0, a new major release of a software tool for the synthesis of certificates (e.g., Lyapunov and barrier functions) for dynamical systems modelled as ordinary differential and difference equations. Fossil 2.0 is much improved from its original release, including new interfaces, a significantly expanded certificate...

ARCH-COMP23 Category Report: Stochastic Models

Abstract<br/>This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year’s edition of the competition. Given that the tools for stochastic...

Inner approximations of stochastic programs for data-driven stochastic barrier function design

This paper proposes a new framework to compute finite-horizon safety guarantees for discrete-time piece-wise affine systems with stochastic noise of unknown distributions. The approach is based on a novel approach to synthesise a stochastic barrier function (SBF) from noisy data and rely on the scenario optimization theory. In particular, we...

ARCH-COMP22 Category Report: Stochastic Models

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks and their properties within this category and recommends next steps for this category towards next year’s edition of the competition. In comparison with tools on non-probabilistic models,...

ARCH-COMP21 Category Report: Stochastic Models

This report presents the results of a friendly competition for formal verification and<br/>policy synthesis of stochastic models. It also introduces new benchmarks within this category, and recommends next steps for this category towards next year's edition of the competition. The friendly competition took place as part of the workshop Applied...

ARCH-COMP20 Category Report: Stochastic Models

This report presents the results of a friendly competition for formal verification and<br/>policy synthesis of stochastic models. It also introduces new benchmarks within this<br/>category, and recommends next steps for this category towards next year's edition of the competition. The friendly competition took place as part of the workshop...

Arch-comp19 category report: Stochastic modelling

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks within this category, and recommends next steps for this category towards next year’s edition of the competition. The friendly competition took place as part of the workshop Applied...

ARCH-COMP18 Category Report: Stochastic Modelling

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In this first edition, we present five benchmarks with different levels of complexities...