What does Imandra do?
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.
How can you use Imandra?
There are two ways to use Imandra: (1) as a stand-alone tool for reasoning about your code written in OCaml/ReasonML, and (2) by incorporating its Reasoning as a Service APIs within a larger application:
1. Write code in OCaml/ReasonML - analyze it with Imandra (e.g. verify its properties) and then use the OCaml/ReasonML compiler toolchain to compile the code to an executable.
2. Using Imandra’s APIs in a larger software - use Imandra as a “powerful calculator”. For example, one application may be for a planning system where the user interface would compose the problem and ask Imandra to solve it.
As a back-end for reasoning about algorithms written in OCaml/ReasonML or a Domain Specific Language (DSL).
Some problems require special languages for describing and reasoning about them. We have 2 examples of domain-specific languages developed as a front-end to Imandra to deal with specific domains. What’s special about these DSLs is that they have a formal semantics defined in Imandra - that is, a syntactically valid program written in the DSLs can be automatically translated into Imandra code that Imandra can reason about.
There are currently two DSLs:
IDF-Py - 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.
Imandra Protocol Language (IPL) - domain specific language for specifying connectivity protocols. We designed this primarily for trading systems, but it’s generic enough that it may be applied to any complex communication protocols.
We have considerable expertise in developing domain-specific languages so don’t hesitate to ask if you have a particular domain that would benefit from this.
Imandra compared to other systems and techniques
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.
Details 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.