15 citations · 28 across the 12 of their papers we have counts for
14 papers
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
Matthew L. Daggitt, Ekaterina Komendantskaya, Alistair Sirman +4
Formal verification of neuro-symbolic cyber-physical systems, such as drones, medical devices and robots, is complicated. Neural components must be trained to be optimal with respe…
Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
Hongyu Lin, Samer Abdallah, Makar Valentinov +5
Large Language Models (LLMs) have shown strong performance on code understanding tasks, yet they fundamentally lack the ability to perform precise, exhaustive mathematical reasonin…
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…
ACL2 Proofs of Nonlinear Inequalities with Imandra
Grant Passmore
We present a proof-producing integration of ACL2 and Imandra for proving nonlinear inequalities. This leverages a new Imandra interface exposing its nonlinear decision procedures.…
Towards a Certified Proof Checker for Deep Neural Network Verification
Remi Desmartin, Omri Isac, Grant Passmore +3
Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for guaranteeing their safety. These…
Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning
John Hester, Briland Hitaj, Grant Passmore +3
Cylindrical Algebraic Decomposition (CAD) is a key proof technique for formal verification of cyber-physical systems. CAD is computationally expensive, with worst-case doubly-expon…