mlsanityData to 7 Oct 2026

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

arXiv 2311.09793 ↗First posted 16 Nov 2023eess.SY cs.LG cs.LOcited by 15

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. Cited by 15 papers in the map (data through 7 Oct 2026). Builds on 12 of its 28 references that are in the map. First posted on arXiv 16 Nov 2023.

Builds on

12 of 28 references.

References · 12

  1. 2022Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methodscited by 148
  2. 2020Neural Lyapunov Controlcited by 142
  3. 2021Stability Verification in Stochastic Control Systems via Neural Network Supermartingalescited by 24
  4. 2022Safety Certification for Stochastic Systems via Neural Barrier Functionscited by 22
  5. 2022Learning Control Policies for Stochastic Systems with Reach-avoid Guaranteescited by 21
  6. 2020Automated and Sound Synthesis of Lyapunov Functions with SMT Solverscited by 10
  7. 2023A General Framework for Verification and Control of Dynamical Models via Certificate Synthesiscited by 6
  8. 2015Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay Propertiescited by 3
  9. 2013SOSTOOLS Version 4.00 Sum of Squares Optimization Toolbox for MATLABcited by 2
  10. 2020Formal Synthesis of Lyapunov Neural Networkscited by 2
  11. 2020Formal controller synthesis for hybrid systems using genetic programmingcited by 2
  12. 2018Formal Synthesis of Analytic Controllers for Sampled-Data Systems via Genetic Programmingcited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 3; 2025: 6; 2026: 6.

15 papers.

Sort:

By area:

  1. 2024Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformerscited by 29
  2. 2024Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificatescited by 15
  3. 2025Two-Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansioncited by 6
  4. 2024Formally Verified Physics-Informed Neural Control Lyapunov Functionscited by 4
  5. 2025Safe Domains of Attraction for Discrete-Time Nonlinear Systems: Characterization and Verifiable Neural Network Estimationcited by 3
  6. 2025Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagationcited by 2
  7. 2025LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systemscited by 2
  8. 2025Analytical Lyapunov Function Discovery: An RL-based Generative Approachcited by 1
  9. 2026Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorialcited by 1
  10. 2025Neural Proofs for Sound Verification and Control of Complex Systemscited by 0
  11. 2026Kernel-Based Learning of Safety Barrierscited by 0
  12. 2026Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systemscited by 0
3 more
  1. 2026k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamicscited by 0
  2. 2026Certificate-Guided Evaluation of Reinforcement Learning Generalizationcited by 0
  3. 2026Neural Slack Variables for Shape Constraintscited by 0