Abstract:

Imandra (imandra.ai) is a cloud-native automated reasoning system powering a suite of tools for the design and regulation of complex algorithms. Imandra is finding exciting industrial use: For example, Goldman Sachs is now public with the fact that Imandra is used to design and audit some of their most complex trading algorithms.

Foundationally, Imandra is a full-featured interactive theorem prover with a unique combination of features, including: an “executable” logic based on a (pure, higher-order) subset of OCaml (in much the same way that ACL2’s logic is based on a subset of Lisp), first-class computable counterexamples (with a proof procedure that is “complete for counterexamples” in a precise sense), a seamless integration of bounded model checking and full-fledged theorem proving, decision procedures for nonlinear real and floating point arithmetic, first-class state-space decompositions, and powerful techniques for automated induction (including the “lifting” of many Boyer-Moore ideas to our typed, higher-order setting).

In this talk, I’ll give an overview of Imandra and we’ll together work many examples. You can follow along and experiment with Imandra in the browser at http://try.imandra.ai/ and install Imandra locally by following the instructions at http://docs.imandra.ai/.

Biography:

Grant Passmore is co-founder and co-CEO of Imandra Inc. (imandra.ai) where he leads the development of the Imandra automated reasoning system. Grant is a widely published researcher in formal verification and symbolic AI, with work ranging from nonlinear decision procedures in SMT to the analysis of fairness and regulatory compliance of financial algorithms. He has been a key contributor to safety verification of algorithms at Cambridge, Carnegie Mellon, Edinburgh, Microsoft Research and SRI. He earned his PhD from the University of Edinburgh, is a graduate of UT Austin (BA in Mathematics) and the Mathematical Research Institute in the Netherlands (Master Class in Mathematical Logic), and is a Life Member of Clare Hall, University of Cambridge.