Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models
Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control(2023)
摘要
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 SMT 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要