This paper introduces Fossil 2.0, an advanced software tool designed for synthesizing certificates such as Lyapunov and barrier functions for dynamical systems represented by ordinary differential equations and difference equations. Fossil 2.0 features a range of significant enhancements, including improved user interfaces, an expanded library of certificates, controller synthesis capabilities, and an extensible architecture. These advancements are detailed as part of this paper. The core of Fossil is a counterexample-guided inductive synthesis (CEGIS) framework that ensures soundness. The tool employs neural networks as templates to generate candidate functions, which are rigorously validated using a satisfiability modulo theories (SMT) solver. Key improvements over the previous release include support for a broader class of certificates, integration of control law synthesis, and compatibility with discrete-time 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 portfolio, controller synthesis and enhanced extensibility. We present these new features as part of this tool paper. Fossil implements a counterexample-guided inductive synthesis (CEGIS) loop ensuring the soundness of the method. Our tool uses neural networks as templates to generate candidate functions, which are then formally proven by an satisfiability modulo theories solver acting as an assertion verifier. Improvements with respect to the first release include a wider range of certificates, synthesis of control laws, and support for discrete-time models.

No abstract available.

This paper accompanies FOSSIL: a software tool for the synthesis of Lyapunov functions and of barrier certificates (or functions) for dynamical systems modelled as differential equations. Lyapunov functions are formal certificates for stability analysis, whereas barrier functions are formal certificates for the safety of dynamical models. FOSSIL is sound and automatic thanks to a counterexample-guided inductive synthesis loop. This method exploits the flexibility of candidate functions generated by training neural network templates, the formal assertions provided by a verifier (namely, an SMT solver), and finally new procedures to ease the exchange of information between the two mentioned components. We endow the tool with features of usability, scalability, and robustness---all of which are showcased on benchmarks.

Abstract We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The approach is underpinned by an inductive framework: this is structured as a sequential loop between a learner, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate’s validity or generates counter-examples to further guide the learner. We compare the approach against state-of-the-art techniques, over polynomial and non-polynomial dynamical models: the outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine (up to three orders less), whilst needing a far smaller data set (up to three orders less) for the learning part. Beyond improvements over the state of the art, we further challenge the new approach on a hybrid dynamical model and on larger-dimensional models, and showcase the numerical robustness of our algorithms and codebase.

In this paper we employ SMT solvers to soundly synthesise Lyapunov functions that assert the stability of a given dynamical model. The search for a Lyapunov function is framed as the satisfiability of a second-order logical formula, asking whether there exists a function satisfying a desired specification (stability) for all possible initial conditions of the model. We synthesise Lyapunov functions for linear, non-linear (polynomial), and for parametric models. For non-linear models, the algorithm also determines a region of validity for the Lyapunov function. We exploit an inductive framework to synthesise Lyapunov functions, starting from parametric templates. The inductive framework comprises two elements: a learner proposes a Lyapunov function, and a verifier checks its validity - its lack is expressed via a counterexample (a point over the state space), for further use by the learner. Whilst the verifier uses the SMT solver Z3, thus ensuring the overall soundness of the procedure, we examine two alternatives for the learner: a numerical approach based on the optimisation tool Gurobi, and a sound approach based again on Z3. The overall technique is evaluated over a broad set of benchmarks, which shows that this methodology not only scales to 10-dimensional models within reasonable computational time, but also offers a novel soundness proof for the generated Lyapunov functions and their domains of validity.