Making Algorithms Safe and Fair
Algorithms manage everything from aircraft autopilot systems and financial exchanges to blockchain smart contracts and smart phone apps. Imandra analyses algorithms to help you understand what they do, why they do it, and what can possibly go wrong.
1 | Modern Software
Software continues to improve communication and commerce around the world. But these improvements come with significant risk. Regulators, businesses, and the general public urgently need to manage the risks these ubiquitous systems present, as they fly our airplanes, run our smart phone apps, and execute blockchain smart contracts.
2 | Ambiguity and Complexity
Documents describing how complex systems work are often rife with mistakes and ambiguity. We need better means for communicating about how complex algorithms are designed. To this end Imandra leverages formal verification – a mathematical science dedicated to describing and reasoning rigorously about algorithms – to help accurately predict how software should and will behave.
3 | Cloud Ecosystem
Imandra’s cloud infrastructure marries software documentation and the power of formal verification, providing the first collaborative environment for translating complex algorithms into mathematical models, applying powerful tools to reason about them. Our cloud also incorporates multiple Domain Specific Languages (DSLs), libraries of common properties relevant to financial regulations, models of common system components, and tools for collaborative analysis.
4 | Mathematical Models
Given a model and a property to reason about, Imandra works to generate a proof that the property will always hold, or to present a concrete counterexample identifying how the property may be violated. For complex systems such counterexamples often identify nontrivial sequences of events that are virtually undiscoverable by hand (or with random number generators).
5 | Automated Reasoning
Many modern systems operate across virtually infinite state spaces. In other words, all the ways a piece of software could potentially behave are incomprehensible to any person or team. At its core, Imandra employs powerful automated theorem proving techniques to analyse and reason about complex algorithms. Imandra brings tools traditionally reserved for highly specialised teams at institutions like NASA to the general public.
6 | Governance, Safety, Fairness
Imandra’s deep algorithmic analysis makes effective governance of the modern algorithmic world possible. From financial algorithms to self-driving cars, our mission is to revolutionise safety and fairness of industries that run on algorithms.
AUTOMATED THEOREM PROVING
NONLINEAR DECISION PROCEDURES
SATISFIABILITY MODULO THEORIES
AUTOMATED COMPLIANCE REPORTS
TEST SUITE GENERATION