Applications
Let’s now dive into the specifics with links to various interactive examples. As already discussed, Imandra has two core applications: formal verification and symbolic reasoning. Here we present both with relevant examples:
1. FORMAL VERIFICATION
FV is a well-established field built around the mathematical verification of algorithm properties. Historically, and especially as it’s applied to verification of general software, this was a very manual effort requiring years of specialized training (PhD). Imandra is changing this.
The following are examples applications of Imandra verifying properties from different domains. You will notice that (1) you use the same language to write programs and properties you wish to verify, and (2) the level of FV expertise required to use Imandra and get results is minimal; indeed, we believe an typical engineering or computer science graduate can easily make serious use of Imandra out of the box.
Verifying a hardware component
Verifying a Robot OS node
We also have several Medium blog posts on the subject:
Imandra interface to Robot OS: Part II
Probabilistic reasoning in ReasonML
Verifying Merge Sort
2. SYMBOLIC REASONING
STATE-SPACE DECOMPOSITION: Region Decomposition is inspired by Cylindrical Algebraic Decomposition, a fundamental technique for reasoning about nonlinear polynomial systems by decomposing Euclidean space into a finite number of connected regions s.t. within each region the behavior of the system under analysis is invariant. This effectively computes a “map” of all possible behaviors of the system, and facilitates a wide variety of nonlinear
decision procedures over the reals and complexes.
Read a high-level overview
Here are some of the use cases:
Testing - when it comes to testing complex systems, everyone agrees that they should be tested ‘thoroughly’, but what does that mean? What’s a scientifically-grounded technique for describing ‘thoroughness’? With Region Decomposition, you get precisely this - a quantitative measure of a system state-space. The Regions in this case represent the quantitative analogs of ‘edge cases’ that engineers typically construct ‘by hand’ or with help of random number generators.
Model-based engineering - Imandra paves way to true model-based development (MBE). A model developed in Imandra is:
● Susceptible to formal verification as discussed above
● Executable, so may be co-simulated with the actual implementation to audit performance
● May be used to automatically generate test cases with quantitative coverage metrics, through the application of Imandra’s Region Decomposition machinery.
Autonomous systems - as autonomous systems become ubiquitous, it is evermore important to ensure they’re tested thoroughly. Reliable simulation environments are used to test algorithms before they’re deployed in the real-world. But the question remains: how do we reason about thoroughness of the tests that these systems are subjected to? With Imandra, you may develop a model of the physical environment and derive the symbolic edge cases (or regions), and translate them
into testing scenarios targeting specific simulation environments.
Explainability/Documentation generation - when Imandra computes regions, it reflects them back into the runtime so you may compute with them. We have example where we translate region descriptions into English-like prose which may serve as precise and automatically generated documentation of a model. In fact, our clients in financial services already rely on this technique for generating up-to-date and thorough documentation.
Reinforcement learning - when you’re training an image classifier, it’s important to make sure the training data is diverse. No single class is over-represented or under-represented. Any skew in the training data will lead to a bias in the classifier. How do we translate this to decision controllers trained using Reinforcement learning? Imandra’s Region Decomposition provides a methodology for ensuring the training of
reinforcement learning algorithms is diverse. Naturally, this leads to better performance and faster convergence. We have results to demonstrate this which we can share if you’re interested. Moreover, we have developed a Python interface (discussed below) to make it easy to use Imandra together with the popular NN libraries like TensorFlow.
Planning - in complex domains, it may be the case that there are no ‘good’ solutions and the operator has to choose one among many and understand why those options were presented. Imandra is uniquely positioned to not only solve both traditional and highly nontraditional planning problems (e.g., through its decision procedures for recursive function unrolling integrated with SMT solving), but also to leverage its symbolic reasoning to explore, compare and explain the
full spectrum of possible outcomes and generate concrete plans to accomplish them.
CONSTRAINT SOLVING - some problems require much more powerful means of expressing problems than what traditional constraint solvers provide. Imandra treats code as mathematical logic, allowing you to encode even the most complex problems as executable programs which can then be automatically analyzed with respect to a rich language of constraints (including recursive functions, higher-order functions,
nonlinear real and floating point arithmetic and more):
Examples of Imandra solving constraints:
Sudoku
OPTIMIZATION - similarly to constraint solving discussed above, Imandra may be used to search for a solution that not only satisfies a specified set of non-trivial constraints, but also maximizes (or minimizes) a specific penalty function. We will have examples of these solutions soon.
Use cases
There are 3 ways to use Imandra: (1) as a stand-alone tool for reasoning about code written in OCaml/ReasonML, (2) creating a Domain Specific Language (DSL) that translates into OCaml and is analyzed by Imandra, and (3) by integrating Imandra's Reasoning as a Service(r) APIs into a larger application:
1. A stand-alone tool for reasoning about code written in OCaml/ReasonML
OCaml is a great open source general programming language. For its pure subset we have created mechanized formal semantics - code written in this pure subset Imandra automatically translates into axiomatic representation and analyzes. Imandra operates in two 'modes' - 'logic' for analyzing the pure subset of OCaml and 'program' which allows you to write impure OCaml code that
interacts with 'logic' mode. This flexibility allows you to write powerful applications leveraging automated reasoning. ReasonML is a new language built on OCaml designed primarily for web development (e.g. Facebook Messenger is written in ReasonML) which Imandra now supports.
2. Create a Domain Specific Language (DSL) "on top of" Imandra
While OCaml/ReasonML are great general programming languages, many types of problems benefit from Domain Specific Languages.
We have two examples of such languages - PyIDF and Imandra Protocol Language (IPL):
2.1. PyIDF is a Python interface to our Iterative Decomposition Framework (Region Decomposition optimized for analysis of multi-step behavior of state machines). We created the Python interface
to make this easily accessible for machine learning/AI developers.
2.2. IPL is a domain specific language for encoding system connectivity protocols. We designed it primarily for trading systems, but it's generic enough to be applied to any complex system.
Our team has incredible language design and development expertise, so if you have a specific project in mind, please do not hesitate to contact us (contact@imandra.ai).
3. Integrate Imandra Core's APIs into another application
Imandra Core's reasoning power may be seamlessly integrated into your application through its Reasoning as a Service(R) APIs. Imandra Core's features like region decomposition, constraint solving and optimization (mixing continuous and discrete decision variables) offer unprecedented capabilities for applications across numerous industries.
One example of such integration is our IPL Simulator product where a user can turn any IPL (Imandra Protocol Language) model into an on-demand simulation environment. There, Imandra automatically processes the generated model and acts as a library which synthesizes messages in response to user actions.
Installation options
1. Single user local Imandra Core
The simplest way to run Imandra Core is by running it on a local machine either as a Docker container or native executables for *nix operating systems (eg. Mac OS or Linux). Note that this is only available for enterprise and Government users.
2. Single user Imandra Core in a Kubernetes cluster
Imandra is natively designed to take advantage of cloud computing. With Imandra Core running in Kubernetes, it takes advantage of parallelization and caching, significantly speeding up several important classes of queries like region decomposition and formal verification. We provide this as the default environment for our retail customers in Google Cloud and make it available for enterprise and Government users.
3. Multi-tenant Imandra Core in a Kubernetes cluster
Imandra Core caches intermediate results, so running a multi-tenant Kubernetes environment brings further speed improvements as Imandra reuses results from your colleagues' queries. Similarly to the setup #2 above, we provide this for retail customers in the public cloud, and enterprise and government customers (public cloud and on-premise).
Imandra vs.
Boyer-Moore: Like ACL2, Imandra’s logic is based on a mechanized formal semantics for an efficiently executable programming language (for ACL2, this is a first-order fragment of Lisp; for Imandra, this is a higher-order fragment of OCaml/ReasonML). This means that Imandra models are simultaneously executable programs (i.e., valid OCaml/ReasonML) and mathematical artifacts which may be subjected to rigorous formal analysis by Imandra’s
reasoning engine. In Imandra, we have “lifted” many core Boyer-Moore ideas powering their remarkable successes in automating induction and simplification to our typed, higher-order setting.
HOL, Isabelle/HOL, Coq, Agda and Lean: Like provers in the HOL family (as well as those based on dependent types such as Coq, Agda and Lean), Imandra’s logic is strongly typed. Like HOL systems, Imandra is built upon a higher-order polymorphic type theory (a variant of Hindley-Milner corresponding to pure OCaml). Imandra supports a rich executable fragment of HOL, with automation including efficient higher-order rewriting and induction through first-order
specialization.
SAT and SMT: Like SMT solvers, Imandra contains orchestrated combinations of high-performance CDCL-based SAT solving and decision procedures for theories relevant to program analysis. Crucially, Imandra’s proof procedures support the synthesis of reflected executable counterexamples (even of higher-order goals requiring function synthesis). All counterexamples constructed by Imandra are “first-class,” i.e., executable and available in the same runtime environment as
the formal models themselves. This allows rapid prototyping iteration and model diagnostics, as counterexamples can be directly run through models. Imandra lifts SMT from (non-executable, monomorphic) first-order logic without recursion and induction to a rich executable, polymorphic higher-order logic with recursion and induction.
Integration of Model Checking and Theorem Proving: Imandra seamlessly integrates bounded model checking (lifted to operate modulo higher-order recursive functions over algebraic datatypes, integers, reals, etc.) and “full-fledged” interactive theorem proving. Every verification goal in Imandra may be analyzed in “bounded” and “unbounded” fashions, and bounded results may be turned into actual theorems (e.g., incorporating bounds on the datatypes involved explicitly in theorem
hypotheses) automatically. This allows for powerful incremental approaches to verification, utilizing bounded verification to rapidly eliminate design flaws,“completing” the results to their unbounded form as necessary only after all flaws corresponding to counterexamples found by bounded verification attempts have been eliminated.
Nonlinear Decision Procedures for Hybrid Systems: Imandra has deep support for datatypes and decision procedures relevant to the analysis of hybrid systems. This includes model-producing decision procedures for the existential theory of real closed fields (nonlinear real arithmetic w.r.t. systems of many-variable nonlinear polynomial equations and inequalities) integrated with Imandra’s inductive “waterfall” proof procedure. Moreover, Imandra can natively compute with
and reason about real algebraic numbers. Through our experience working with (and in many cases contributing to) hybrid systems verification tools such as KeYmaera, Flow*, dReal and dReach and HybridSAL, we recognize scalable nonlinear real decision procedures as one of the most important bottlenecks in hybrid systems verification. The derivation of computable counterexamples (dually, instances in the case of test-case generation) satisfying constraints on both the discrete and
continuous components of the models is crucial to efficient V&V.
More on Region Decomposition
Region decomposition lifts CAD to algorithms through a combination of symbolic execution, automated induction and nonlinear decision procedures. The result is an automatic method for decomposing the state-space of a system (as given by the “step” function of an (infinite) state-machine) into a finite number of symbolically described regions s.t. (a) the union of all regions covers the entire state-space, and (b) in each region, the behavior of the system is invariant. Regions decompositions are computed subject to a basis, a collection of function and predicate symbols which are taken as “basic” and will be used in region descriptions, and side-conditions which may express queries to focus the decomposition on specific behaviors (i.e., compute all regions of the state-space s.t. the controller will result in the following bad state). Bases and side-conditions facilitate configurable abstraction boundaries and foci and allow the analysis of the state-space to be adapted for many different applications, from high-coverage test-suite generation to automated documentation synthesis to interactive state-space exploration.