Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Thu 22 Aug 2019 09:00 - 10:00 at Pine - Session 1 Chair(s): KC Sivaramakrishnan

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/.

Thu 22 Aug

mlfamilyworkshop-2019-papers
09:00 - 10:00: ML 2019 - Session 1 at Pine
Chair(s): KC SivaramakrishnanIIT Madras
mlfamilyworkshop-2019-papers09:00 - 10:00
Talk
Grant PassmoreImandra Inc.