Model-Based Software Development with Imandra

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 a 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."

As the famous quip goes, testing can reveal the 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 for highly specialized teams of PhDs at places like NASA. Imandra brings Formal Verification to mass software development.

Imandra's Region Decomposition (RD) is the new (quantitative) standard for testing complex systems. With RD, you can automatically compress (typically virtually infinite) the model's state-space 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 the behavior of the decompose model or fragment of the model. Imandra will generate test vectors for each region - giving you the most rigorous means (with explanations) of generating test cases.

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 the operation of systems in production. You can take it a step further by studying the model's behavior in response to different inputs and use this to calibrate the decisions it makes.