Welcome to

# Imandra Core

Gallery

Welcome mighty programmer! Here you'll find a sorted selection of many Imandra demo examples. We have prepared three different grouping options to help you find the right starting point.

Sort Demos by:

## Beginner

## Analysing Web-app Authentication Logic

In this notebook, we look at some typical authentication logic found in a standard web application and analyze it with Imandra to make sure it's doing what we expect.

Learn more

## Simple Vehicle Controller

In this notebook, we'll design and verify a simple autonomous vehicle controller in Imandra. The controller we analyze is due to Boyer, Green, and Moore and is described and analyzed in their article "The Use of a Formal Simulator to Verify a Simple Real-Time Control Program".

Learn more

## Simple Car Intersection Model

In this notebook, we'll implement a simple model of a road intersection with a car approaching. We'll then use Imandra's Principal Region Decomposition to explore its state-space and define custom printers to examine the behavior of a car approaching the intersection using English prose.

Learn more

## Tic Tac Toe with ReasonML

ReasonML provides an alternative syntax for OCaml, which Imandra can read. Let's walk through an example ReasonML model of Tic Tac Toe and use Imandra to understand and verify some of its properties.

Learn more

## Exploring The Apple FaceTime Bug with ReasonML State Machines

In this notebook we explore the Apple FaceTime bug and different ways of modelling our applications as state machines.

Learn more

## Crossing the River Safely

For the sake of brain-scrambling, we're going to solve this ancient puzzle using Imandra (again!). As most polyvalent farmers will tell you, going to the market with your pet wolf, tastiest goat, and freshest cabbage is sometimes difficult as they tend to have an appetite for one another. The good news is that there is a way to cross this river safely anyway.

Learn more

## Intermediate

## Analysing the UBS ATS dark pool

In this notebook, we model the order priority logic of the UBS ATS dark pool described in UBS's June 1st, 2015 Form ATS submission to the SEC and analyze it using Imandra. We observe that, as described, the order priority logic suffers from a fundamental flaw: the order ranking function is not transitive.

Learn more

## Region Decomposition - Exchange Pricing

In this notebook, we'll use Imandra to model a fragment of the SIX Swiss trading logic and decompose its state-space using region decomposition.

Learn more

## Creating and Verifying a ROS Node

At AI, we've been working on an IML (Imandra Modeling Language) interface to ROS, allowing one to develop ROS nodes and use Imandra to verify their properties. In this notebook, we will go through the creation and verification of a Robotic Operating System (ROS) node in Imandra. We will make a robot control node that controls the motion of a simple 2-wheeler bot.

Learn more

## Key Pair Security in Imandra

In this ReasonML notebook, we use Imandra to quickly discover the "man in the middle" attack for protocols with private/public key exchange protocols.

Learn more

## Solving Sudoku with Imandra

We're going to define what is a sudoku puzzle, and how to check if given sudoku is solvable. From that, we can get Imandra to find solutions for us without actually writing a sudoku solver.

Learn more

## Synthesising a Game Solver in Imandra

In this notebook, we introduce a simple game called "Les Bâtonnets Géants" and show how Imandra can be exploited to synthesize a strategy that always wins.

Learn more

## Exchange implied trading

In this example, we create a simple multi-book venue with synthetic securities expressed as a linear combination of underlying securities. We show how one can reason about their interaction and cross-trading.

Learn more

## COVID 19: School scheduling facilitating social distancing

In this notebook, we employ Imandra's abilities to solve scheduling problems to facilitate social distancing.

Learn more

## Advanced

## Recursion, Induction, and Rewriting

In this notebook, we're going to use Imandra to prove some interesting properties of functional programs. We'll learn a bit about induction, lemmas and rewrite rules along the way.

Learn more

## Verifying Merge Sort in Imandra

Merge sort is a widely used efficient general-purpose sorting algorithm and a prototypical divide and conquer algorithm. It forms the basis of standard library sorting functions in languages like OCaml, Java, and Python. Let's verify it with Imandra!

Learn more

## Verifying a Ripple Carry Adder

In this notebook, in Imandra, we'll verify a simple hardware design of a full (arbitrary width) ripple-carry adder. We'll express this simple piece of hardware at the gate level. The theorem we'll prove expresses that our (arbitrary width) adder circuit is correct for all possible bit sequences.

Learn more

## Calculating Region Probabilities

This notebook introduces a small probabilistic programming library that allows users to reason about Imandra Modeling Language (IML) models probabilistically.

Learn more

## Analysing Machine Learning Models With Imandra

This notebook shows how Imandra can analyze and reason about models learned from data, an important and exciting topic bridging the gap between formal methods and machine learning.

Learn more

## Probabilistic reasoning in ReasonML

In this ReasonML notebook, we employ Imandra's ability to reason about functional values to analyze probabilistic scenarios following the example of the Monty Hall problem (there is also an OCaml in this notebook).

Learn more

## A comparison with TLA+

In this notebook, we encode examples from the Learn TLA+ book in Imandra.

Learn more

## Formal Verification

## Simple Vehicle Controller

In this notebook, we'll design and verify a simple autonomous vehicle controller in Imandra. The controller we analyze is due to Boyer, Green, and Moore and is described and analyzed in their article "The Use of a Formal Simulator to Verify a Simple Real-Time Control Program".

Learn more

## Tic Tac Toe with ReasonML

ReasonML provides an alternative syntax for OCaml, which Imandra can read. Let's walk through an example ReasonML model of Tic Tac Toe and use Imandra to understand and verify some of its properties.

Learn more

## Exploring The Apple FaceTime Bug with ReasonML State Machines

In this notebook we explore the Apple FaceTime bug and different ways of modelling our applications as state machines.

Learn more

## Analysing the UBS ATS dark pool

In this notebook, we model the order priority logic of the UBS ATS dark pool described in UBS's June 1st, 2015 Form ATS submission to the SEC and analyze it using Imandra. We observe that, as described, the order priority logic suffers from a fundamental flaw: the order ranking function is not transitive.

Learn more

## Creating and Verifying a ROS Node

At AI, we've been working on an IML (Imandra Modeling Language) interface to ROS, allowing one to develop ROS nodes and use Imandra to verify their properties. In this notebook, we will go through the creation and verification of a Robotic Operating System (ROS) node in Imandra. We will make a robot control node that controls the motion of a simple 2-wheeler bot.

Learn more

## Key Pair Security in Imandra

In this ReasonML notebook, we use Imandra to quickly discover the "man in the middle" attack for protocols with private/public key exchange protocols.

Learn more

## Exchange implied trading

In this example, we create a simple multi-book venue with synthetic securities expressed as a linear combination of underlying securities. We show how one can reason about their interaction and cross-trading.

Learn more

## Recursion, Induction, and Rewriting

In this notebook, we're going to use Imandra to prove some interesting properties of functional programs. We'll learn a bit about induction, lemmas and rewrite rules along the way.

Learn more

## Verifying Merge Sort in Imandra

Merge sort is a widely used efficient general-purpose sorting algorithm and a prototypical divide and conquer algorithm. It forms the basis of standard library sorting functions in languages like OCaml, Java, and Python. Let's verify it with Imandra!

Learn more

## Verifying a Ripple Carry Adder

In this notebook, in Imandra, we'll verify a simple hardware design of a full (arbitrary width) ripple-carry adder. We'll express this simple piece of hardware at the gate level. The theorem we'll prove expresses that our (arbitrary width) adder circuit is correct for all possible bit sequences.

Learn more

## Analysing Machine Learning Models With Imandra

This notebook shows how Imandra can analyze and reason about models learned from data, an important and exciting topic bridging the gap between formal methods and machine learning.

Learn more

## A comparison with TLA+

In this notebook, we encode examples from the Learn TLA+ book in Imandra.

Learn more

## Region Decomposition

## Simple Car Intersection Model

In this notebook, we'll implement a simple model of a road intersection with a car approaching. We'll then use Imandra's Principal Region Decomposition to explore its state-space and define custom printers to examine the behavior of a car approaching the intersection using English prose.

Learn more

## Region Decomposition - Exchange Pricing

In this notebook, we'll use Imandra to model a fragment of the SIX Swiss trading logic and decompose its state-space using region decomposition.

Learn more

## Calculating Region Probabilities

This notebook introduces a small probabilistic programming library that allows users to reason about Imandra Modeling Language (IML) models probabilistically.

Learn more

## Probabilistic reasoning in ReasonML

In this ReasonML notebook, we employ Imandra's ability to reason about functional values to analyze probabilistic scenarios following the example of the Monty Hall problem (there is also an OCaml in this notebook).

Learn more

## Constraint Solving

## Crossing the River Safely

For the sake of brain-scrambling, we're going to solve this ancient puzzle using Imandra (again!). As most polyvalent farmers will tell you, going to the market with your pet wolf, tastiest goat, and freshest cabbage is sometimes difficult as they tend to have an appetite for one another. The good news is that there is a way to cross this river safely anyway.

Learn more

## Solving Sudoku with Imandra

We're going to define what is a sudoku puzzle, and how to check if given sudoku is solvable. From that, we can get Imandra to find solutions for us without actually writing a sudoku solver.

Learn more

## Synthesising a Game Solver in Imandra

In this notebook, we introduce a simple game called "Les Bâtonnets Géants" and show how Imandra can be exploited to synthesize a strategy that always wins.

Learn more

## COVID 19: School scheduling facilitating social distancing

In this notebook, we employ Imandra's abilities to solve scheduling problems to facilitate social distancing.

Learn more

## Autonomous Systems

## Simple Vehicle Controller

In this notebook, we'll design and verify a simple autonomous vehicle controller in Imandra. The controller we analyze is due to Boyer, Green, and Moore and is described and analyzed in their article "The Use of a Formal Simulator to Verify a Simple Real-Time Control Program".

Learn more

## Simple Car Intersection Model

In this notebook, we'll implement a simple model of a road intersection with a car approaching. We'll then use Imandra's Principal Region Decomposition to explore its state-space and define custom printers to examine the behavior of a car approaching the intersection using English prose.

Learn more

## Creating and Verifying a ROS Node

At AI, we've been working on an IML (Imandra Modeling Language) interface to ROS, allowing one to develop ROS nodes and use Imandra to verify their properties. In this notebook, we will go through the creation and verification of a Robotic Operating System (ROS) node in Imandra. We will make a robot control node that controls the motion of a simple 2-wheeler bot.

Learn more

## Financial Markets

## Analysing the UBS ATS dark pool

In this notebook, we model the order priority logic of the UBS ATS dark pool described in UBS's June 1st, 2015 Form ATS submission to the SEC and analyze it using Imandra. We observe that, as described, the order priority logic suffers from a fundamental flaw: the order ranking function is not transitive.

Learn more

## Region Decomposition - Exchange Pricing

In this notebook, we'll use Imandra to model a fragment of the SIX Swiss trading logic and decompose its state-space using region decomposition.

Learn more

## Exchange implied trading

In this example, we create a simple multi-book venue with synthetic securities expressed as a linear combination of underlying securities. We show how one can reason about their interaction and cross-trading.

Learn more

## Machine Learning

## Calculating Region Probabilities

This notebook introduces a small probabilistic programming library that allows users to reason about Imandra Modeling Language (IML) models probabilistically.

Learn more

## Analysing Machine Learning Models With Imandra

This notebook shows how Imandra can analyze and reason about models learned from data, an important and exciting topic bridging the gap between formal methods and machine learning.

Learn more

## Probabilistic reasoning in ReasonML

In this ReasonML notebook, we employ Imandra's ability to reason about functional values to analyze probabilistic scenarios following the example of the Monty Hall problem (there is also an OCaml in this notebook).

Learn more

## Other

## Crossing the River Safely

For the sake of brain-scrambling, we're going to solve this ancient puzzle using Imandra (again!). As most polyvalent farmers will tell you, going to the market with your pet wolf, tastiest goat, and freshest cabbage is sometimes difficult as they tend to have an appetite for one another. The good news is that there is a way to cross this river safely anyway.

Learn more

## Solving Sudoku with Imandra

We're going to define what is a sudoku puzzle, and how to check if given sudoku is solvable. From that, we can get Imandra to find solutions for us without actually writing a sudoku solver.

Learn more

## Synthesising a Game Solver in Imandra

In this notebook, we introduce a simple game called "Les Bâtonnets Géants" and show how Imandra can be exploited to synthesize a strategy that always wins.

Learn more

## Recursion, Induction, and Rewriting

In this notebook, we're going to use Imandra to prove some interesting properties of functional programs. We'll learn a bit about induction, lemmas and rewrite rules along the way.

Learn more

## Verifying Merge Sort in Imandra

Merge sort is a widely used efficient general-purpose sorting algorithm and a prototypical divide and conquer algorithm. It forms the basis of standard library sorting functions in languages like OCaml, Java, and Python. Let's verify it with Imandra!

Learn more

## Verifying a Ripple Carry Adder

In this notebook, in Imandra, we'll verify a simple hardware design of a full (arbitrary width) ripple-carry adder. We'll express this simple piece of hardware at the gate level. The theorem we'll prove expresses that our (arbitrary width) adder circuit is correct for all possible bit sequences.

Learn more

## A comparison with TLA+

In this notebook, we encode examples from the Learn TLA+ book in Imandra.

Learn more

## Web Apps

## Analysing Web-app Authentication Logic

In this notebook, we look at some typical authentication logic found in a standard web application and analyze it with Imandra to make sure it's doing what we expect.

Learn more

## Tic Tac Toe with ReasonML

ReasonML provides an alternative syntax for OCaml, which Imandra can read. Let's walk through an example ReasonML model of Tic Tac Toe and use Imandra to understand and verify some of its properties.

Learn more

## Exploring The Apple FaceTime Bug with ReasonML State Machines

In this notebook we explore the Apple FaceTime bug and different ways of modelling our applications as state machines.

Learn more

## COVID 19: School scheduling facilitating social distancing

In this notebook, we employ Imandra's abilities to solve scheduling problems to facilitate social distancing.

Learn more