Software Engineering
with Imandra



Our clients on-average reduced project time to market by over 6 months.



Imandra employs a myriad of cutting-edge AI techniques for rigorous analysis of model properties and automated test suite generation.



MBSE connects your verified model with the actual production system, giving you unprecedented insight into how your systems are deployed and operated.

Applying MBSE to your development process means connecting all of the stakeholders over mathematically precise executable model.

The result is that you have a single source of truth - that you can run, formally verify, use to auto-generate test cases and much more.

Imandra transformation illustration

Further details and features

Imandra Model-Based Software Engeneering

State Dynamics Analysis

When designing complex software, it's important to understand how it may behave. Imandra's Abstractor analyzes and visualizes possible state transitions of your models. Typically models of "real world" software may be in virtually infinite number of possible states, Imandra's Abstractor summarizes them into a finite number of symbolic states. This is the ultimate de-risker of the 'unknown unknowns.'

Imandra Model-Based Software Engeneering - State Dynamics Analysis

Ensuring Design with Formal Verification

Imandra Model-Based Software Engeneering - Formal Methods

As the famous quip goes, testing can reveal presence of bugs but not their absence. This is why our clients formally verify their design to cover infinitely many possible inputs and scenarios to ensure the design meets everyone's expectations - business users, compliance, sales and regulators. Historically, formal verification was reserved to highly specialized teams of PhDs at places like NASA. Imandra brings Formal Verification to mass software development.

Imandra Model-Based Software Engeneering - Formal Methods

Rigorous Testing

With Imandra's Region Decomposition (RD) is the new (quantitative) standard for testing complex systems. With RD, you can automatically compress (typically virtually infinite) state-space of the model into a finite number of symbolic regions. Each region is described by a set of constraints and an invariant result. Together, the regions fully replicate behavior of the decompose model or fragment of the model. For each region, Imandra will generate test vectors - giving you the most rigorous means (with explanations) of generating test cases.

Imandra Model-Based Software Engeneering - Rigorous Testing

Audit and Calibration

Imandra Model-Based Software Engeneering - Simulation and Calibration

Since the model is executable, we can run it on the actual production data to audit the implementation. You can execute the model on the recreated inputs into the system and compare the results of the model's execution against what happened in production. We've built web-based audit and monitoring tools to bring unprecedented insight into operation of systems in production. You can take it a step further by studying behavior of the model in response to different inputs and use this to calibrate the decisions it makes.

Imandra Model-Based Software Engeneering - Simulation and Calibration

Governance and Documentation

A formal model that is verified and reconcilable against production data is the rigorous. In fact, many regulators already either require or encourage Model-Based approaches. When used with Region Decomposition, the model becomes a source of documentation, explaining intricate behaviors in English-prose.

Imandra Model-Based Software Engeneering - Documentation and Governance
By using this website, you agree to our cookie policy

Please note that the Imandra website no longer supports Internet Explorer

We recommend upgrading to the latest Microsoft Edge, Google Chrome, or Firefox