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