Showcases

This showcase demonstrates how to use Isabelle/HOL to reason about probabilistic programs based on the theory we developed.

Uncertainty modelling in RoboChart Probabilistic modelling and verification [RoboChart] using PRISM Probabilistic property language Tool support Automated Reasoning for Probabilistic Programs with Theorem Proving Probabilistic designs Probabilistic relations This poster shows thw work I and my colleagues were or are doing in recent years.

Here we demonstrate the animation of a patrol robot model below using Interaction Trees in Isabelle/HOL. RoboChart model with nondeterministic choice and shared variables The corridor for the robot to patrol has three sections, shown below.

This showcase demonstrates how to use Isabelle/HOL to automatically generate Haskell code (from our manually implemented RoboChart semantics in Isabelle/HOL using interaction trees) for animation.

This showcase demonstrates how RoboTool is used to automatically verify probabilistic behaviour of RoboChart using PRISM.

Uncertainty modelling in RoboChart Probabilistic modelling and verification [RoboChart] using PRISM Probabilistic property language Tool support Automated Reasoning for Probabilistic Programs with Theorem Proving Probabilistic designs Probabilistic relations This poster shows thw work I and my colleagues were or are doing in recent years.