FOSSIL: A software tool for the formal synthesis of lyapunov functions and barrier certificates using neural networks

Abstract

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.