Select Publications
Scientific papers and publications related to Imandra and ImandraX, spanning automated reasoning, formal verification, AI safety, financial systems, and computer arithmetic.
Core System
| Paper | Venue | Year |
|---|---|---|
Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic H. Lin, S. Abdallah, M. Valentinov, P. Brennan, E. Kagan, C.M. Wintersteiger, D. Ignatovich, G.O. Passmore | arXiv | 2026 |
The Imandra Automated Reasoning System (System Description) G.O. Passmore, S. Cruanes, D. Ignatovich, D. Aitken, M. Bray, E. Kagan, K. Sheridan, D. Sheridan, C.M. Sheridan | IJCAR 2020 | 2020 |
Formal Verification of Financial Systems
| Paper | Venue | Year |
|---|---|---|
Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms G.O. Passmore | FM 2021 | 2021 |
Formal Verification of Financial Algorithms G.O. Passmore, D. Ignatovich | CADE 2017 | 2017 |
Case Study: 2015 SEC Fine Against UBS ATS D.A. Ignatovich, G.O. Passmore | Technical Report #AI/1503 | 2015 |
Transparent Order Priority and Pricing D.A. Ignatovich, G.O. Passmore | Technical Report #AI/1502 | 2015 |
Creating Safe and Fair Markets D.A. Ignatovich, G.O. Passmore | Technical Report #AI/1501 | 2015 |
Neural Network Verification & AI Safety
| Paper | Venue | Year |
|---|---|---|
A Certified Proof Checker for Deep Neural Network Verification in Imandra R. Desmartin, O. Isac, G.O. Passmore, E. Komendantskaya, K. Stark, G. Katz | ITP 2025 | 2025 |
Proof-Carrying Neuro-Symbolic Code E. Komendantskaya | CiE 2025 | 2025 |
CheckINN: Wide Range Neural Network Verification in Imandra R. Desmartin, G.O. Passmore, E. Komendantskaya, M.L. Daggitt | PPDP 2022 | 2022 |
Neural Networks in Imandra: Matrix Representation as a Verification Choice R. Desmartin, G.O. Passmore, E. Komendantskaya | LNCS (Springer) | 2022 |
Computer Arithmetic & IEEE Standards
| Paper | Venue | Year |
|---|---|---|
Formal Verification of the IEEE P3109 Standard for Binary Floating-Point Formats for Machine Learning C.M. Wintersteiger | ARITH 2025 | 2025 |
Systems Engineering
| Paper | Venue | Year |
|---|---|---|
Towards the Formal Verification of SysML v2 Models V. Molnar, B. Graics, A. Voros, S. Tonetta, et al. | MODELS 2024 | 2024 |
Usable Security and Verification for Distributed Robotic Systems R.J. White-Magner | UC San Diego (PhD Thesis) | 2021 |
Decision Procedures & Nonlinear Arithmetic
| Paper | Venue | Year |
|---|---|---|
ACL2 Proofs of Nonlinear Inequalities with Imandra G.O. Passmore | ACL2 Workshop 2023 | 2023 |
Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning J. Hester, B. Hitaj, G.O. Passmore, S. Owre, N. Shankar, E. Yeh | CICM 2023 | 2023 |
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers G.O. Passmore | CADE-25 | 2015 |
The Strategy Challenge in SMT Solving L. de Moura, G.O. Passmore | LNCS (Springer) | 2013 |
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals L. de Moura, G.O. Passmore | CADE 2013 | 2013 |
Grobner Basis Construction Algorithms Based on Theorem Proving Saturation Loops G.O. Passmore, L. de Moura, P.B. Jackson | Dagstuhl Seminar | 2010 |