15 citations · 28 across the 12 of their papers we have counts for
Showing 2023Show all
3 papers · 1 filter
cs.LO2023
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.…
cs.LO2023
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…
cs.FL2023
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…