3 papers
cs.PL2026
Verification of a Generational Garbage Collector
Shengyi Wang, Kathrin Stark, Andrew W. Appel
We have formally verified in Rocq+VST a multi-generation collector with support for mutable references, written in C and compatible with OCaml data types. Its carefully specified A…
cs.LO2024
A Certified Proof Checker for Deep Neural Network Verification in Imandra
Remi Desmartin, Omri Isac, Grant Passmore +3
Recent advances in the verification of deep neural networks (DNNs) have opened the way for a broader usage of DNN verification technology in many application areas, including safet…
cs.LO2024
Taming Differentiable Logics with Coq Formalisation
Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya +2
For performance and verification in machine learning, new methods have recently been proposed that optimise learning systems to satisfy formally expressed logical properties. Among…