Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models. Edwards, A., Peruffo, A., & Abate, A. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, of HSCC '24, pages 1–10, New York, NY, USA, May, 2024. Association for Computing Machinery. ![Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models [link]](https://bibbase.org/img/filetypes/link.svg "link")
Paper doi abstract bibtex 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.
@inproceedings{edwards_fossil_2024,
address = {New York, NY, USA},
series = {{HSCC} '24},
title = {Fossil 2.0: {Formal} {Certificate} {Synthesis} for the {Verification} and {Control} of {Dynamical} {Models}},
isbn = {979-8-4007-0522-9},
shorttitle = {Fossil 2.0},
url = {https://dl.acm.org/doi/10.1145/3641513.3651398},
doi = {10.1145/3641513.3651398},
abstract = {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.},
urldate = {2025-10-07},
booktitle = {Proceedings of the 27th {ACM} {International} {Conference} on {Hybrid} {Systems}: {Computation} and {Control}},
publisher = {Association for Computing Machinery},
author = {Edwards, Alec and Peruffo, Andrea and Abate, Alessandro},
month = may,
year = {2024},
pages = {1--10},
}
Downloads: 0
{"_id":"hiubqwK4SvF9XZqjG","bibbaseid":"edwards-peruffo-abate-fossil20formalcertificatesynthesisfortheverificationandcontrolofdynamicalmodels-2024","author_short":["Edwards, A.","Peruffo, A.","Abate, A."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"New York, NY, USA","series":"HSCC '24","title":"Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models","isbn":"979-8-4007-0522-9","shorttitle":"Fossil 2.0","url":"https://dl.acm.org/doi/10.1145/3641513.3651398","doi":"10.1145/3641513.3651398","abstract":"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.","urldate":"2025-10-07","booktitle":"Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control","publisher":"Association for Computing Machinery","author":[{"propositions":[],"lastnames":["Edwards"],"firstnames":["Alec"],"suffixes":[]},{"propositions":[],"lastnames":["Peruffo"],"firstnames":["Andrea"],"suffixes":[]},{"propositions":[],"lastnames":["Abate"],"firstnames":["Alessandro"],"suffixes":[]}],"month":"May","year":"2024","pages":"1–10","bibtex":"@inproceedings{edwards_fossil_2024,\n\taddress = {New York, NY, USA},\n\tseries = {{HSCC} '24},\n\ttitle = {Fossil 2.0: {Formal} {Certificate} {Synthesis} for the {Verification} and {Control} of {Dynamical} {Models}},\n\tisbn = {979-8-4007-0522-9},\n\tshorttitle = {Fossil 2.0},\n\turl = {https://dl.acm.org/doi/10.1145/3641513.3651398},\n\tdoi = {10.1145/3641513.3651398},\n\tabstract = {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.},\n\turldate = {2025-10-07},\n\tbooktitle = {Proceedings of the 27th {ACM} {International} {Conference} on {Hybrid} {Systems}: {Computation} and {Control}},\n\tpublisher = {Association for Computing Machinery},\n\tauthor = {Edwards, Alec and Peruffo, Andrea and Abate, Alessandro},\n\tmonth = may,\n\tyear = {2024},\n\tpages = {1--10},\n}\n\n\n\n\n\n\n\n","author_short":["Edwards, A.","Peruffo, A.","Abate, A."],"key":"edwards_fossil_2024","id":"edwards_fossil_2024","bibbaseid":"edwards-peruffo-abate-fossil20formalcertificatesynthesisfortheverificationandcontrolofdynamicalmodels-2024","role":"author","urls":{"Paper":"https://dl.acm.org/doi/10.1145/3641513.3651398"},"metadata":{"authorlinks":{}},"downloads":0,"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/alukina","dataSources":["Cfgnp5s4HQSBd8tAf"],"keywords":[],"search_terms":["fossil","formal","certificate","synthesis","verification","control","dynamical","models","edwards","peruffo","abate"],"title":"Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models","year":2024}