G. Passmore

Most-cited papers

The Strategy Challenge in SMT Solving
L. D. de Moura, G. Passmore
2013Automated Reasoning and Mathematics66 citations Open access
Semantic Scholar
The Imandra Automated Reasoning System (System Description)
G. Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken +5 more
2020International Joint Conference on Automated Reasoning41 citations Open access
Semantic Scholar
Combined Decision Techniques for the Existential Theory of the Reals
G. Passmore, Paul B. Jackson
2009Calculemus/MKM37 citations Open access
Semantic Scholar
Formal Verification of Financial Algorithms
G. Passmore, Denis Ignatovich
2017CADE31 citations
Semantic Scholar
Combined decision procedures for nonlinear arithmetics, real and complex
G. Passmore
201125 citations
Semantic Scholar
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL
Wenda Li, G. Passmore, Lawrence Charles Paulson
2015Journal of automated reasoning20 citations Open access
Semantic Scholar
Collaborative Verification-Driven Engineering of Hybrid Systems
Stefan Mitsch, G. Passmore, André Platzer
2014Mathematics and Computer Science17 citations Open access
Semantic Scholar
Real Algebraic Strategies for MetiTarski Proofs
G. Passmore, Lawrence Charles Paulson, L. Moura
2012AISC/MKM/Calculemus17 citations Open access
Semantic Scholar
A Certified Proof Checker for Deep Neural Network Verification
Remi Desmartin, Omri Isac, Ekaterina Komendantskaya, Kathrin Stark +2 more
2024International Conference on Interactive Theorem Proving14 citations
Semantic Scholar
Towards a Certified Proof Checker for Deep Neural Network Verification
Remi Desmartin, Omri Isac, G. Passmore, Kathrin Stark +2 more
2023International Workshop/Symposium on Logic-based Program Synthesis and Transformation12 citations Open access
Semantic Scholar
Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms
G. Passmore
2021World Congress on Formal Methods7 citations
Semantic Scholar
Impugning Randomness, Convincingly
Y. Gurevich, G. Passmore
2011Studia Logica: An International Journal for Symbolic Logic7 citations Open access
Semantic Scholar
Superfluous S-polynomials in Strategy-Independent Groebner Bases
G. Passmore, L. D. de Moura
20092009 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing7 citations
Semantic Scholar
On locally minimal Nullstellensatz proofs
L. D. de Moura, G. Passmore
2009International Workshop on Satisfiability Modulo Theories7 citations
Semantic Scholar
CheckINN: Wide Range Neural Network Verification in Imandra
Remi Desmartin, G. Passmore, Ekaterina Komendantskaya, Matthew Daggit
2022ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming6 citations Open access
Semantic Scholar
Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops
G. Passmore, L. D. de Moura, Paul B. Jackson
2010Decision Procedures in Software, Hardware and Bioware6 citations
Semantic Scholar
An Augmented MetiTarski Dataset for Real Quantifier Elimination Using Machine Learning
John Hester, B. Hitaj, G. Passmore, S. Owre +2 more
2023International Conference on Intelligent Computer Mathematics4 citations
Semantic Scholar
Neural Networks in Imandra: Matrix Representation as a Verification Choice
Remi Desmartin, G. Passmore, Ekaterina Komendantskaya
2022NSV/FoMLAS@CAV4 citations Open access
Semantic Scholar
A note on real quantifier elimination by virtual term substitution of unbounded degree
Kristjan Liiva, G. Passmore, Paul B. Jackson
20144 citations
Semantic Scholar
A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems
Stefan Mitsch, G. Passmore, André Platzer
20134 citations
Semantic Scholar
Abstract Partial Cylindrical Algebraic Decomposition I: The Lifting Phase
G. Passmore, Paul B. Jackson
2012Conference on Computability in Europe2 citations
Semantic Scholar
Gröbner Basis Construction Algorithms Based on Superposition Loops
G. Passmore, L. D. de Moura, Paul B. Jackson
20102 citations
Semantic Scholar
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
M. Daggitt, Ekaterina Komendantskaya, Alistair Sirman, Alessandro Bruni +3 more
2026Proc. ACM Program. Lang.1 citations Open access
Semantic Scholar
ACL2 Proofs of Nonlinear Inequalities with Imandra
G. Passmore
2023International Workshop on the ACL2 Theorem Prover and Its Applications1 citations Open access
Semantic Scholar
Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning
John Hester, B. Hitaj, G. Passmore, S. Owre +2 more
2023arXiv.org1 citations Open access
Semantic Scholar
Intelligent Computer Mathematics
Florian Rabe, William M. Farmer, G. Passmore, Abdou Youssef
2018Lecture Notes in Computer Science1 citations
Semantic Scholar
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
G. Passmore
2015CADE1 citations Open access
Semantic Scholar
Collaborative Verification-Driven Engineering of Hybrid Systems
Stefan Mitsch, G. Passmore, André Platzer
2014Mathematics and Computer Science1 citations Open access
Semantic Scholar
Universality of Polynomial Positivity and a Variant of Hilbert ’ s 17 th Problem
G. Passmore, L. D. de Moura, G. Passmore
20091 citations
Semantic Scholar
Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
Hongyu Lin, Samer Abdallah, Makar Valentinov, Paul Brennan +4 more
2026arXiv.org0 citations
Semantic Scholar
Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications
G. Passmore, Ruben Gamboa
2020Electronic Proceedings in Theoretical Computer Science0 citations Open access
Semantic Scholar
Compositional Taylor Model Based Validated Integration
Kristjan Liiva, Paul B. Jackson, G. Passmore, C. Wintersteiger
2018Symposium on Symbolic and Numeric Algorithms for Scientific Computing0 citations Open access
Semantic Scholar
Système et procédé de modélisation et de vérification de plates-formes d'échanges financiers
Denis Ignatovich, G. Passmore
20150 citations
Semantic Scholar
PARTIAL CAD I: THE LIFTING PHASE (EXTENDED TECHNICAL REPORT)
G. Passmore, Paul B. Jackson
20110 citations
Semantic Scholar
Understanding Algebro-Geometric Quantifier Elimination : Part I , Algebraically Closed Fields of Characteristic Zero via Muchnik
G. Passmore
20100 citations
Semantic Scholar
Does SAT exhibit fractal behavior
J. Joosten, G. Passmore
20080 citations
Semantic Scholar
A Continuous Relaxation for Proving Discrete ACL 2 Theorems over Real Closed Fields
Paul B. Jackson, G. Passmore
20080 citations
Semantic Scholar
Diophantine Sets and Their Decision Problems
G. Passmore
20070 citations
Semantic Scholar
Edinburgh Informatics Research Proposal Feasible Arithmetic Proof Procedures, S.M.T., and I.B.M. ∗
G. Passmore
20070 citations
Semantic Scholar