3 papers
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.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…
cs.LO2022
CheckINN: Wide Range Neural Network Verification in Imandra (Extended)
Remi Desmartin, Grant Passmore, Ekaterina Komendantskaya +1
Neural networks are increasingly relied upon as components of complex safety-critical systems such as autonomous vehicles. There is high demand for tools and methods that embed neu…