From time to time we release software as open source, or occasionally under a binary-only licence.
You can find most of our software on github:
The ML-Tool and Isabelle/HOL code that translates a subset of C-99 into something that Isabelle/HOL can understand is available from here.
AutoCorres is an Isabelle/HOL tool that automatically abstracts and simplifies programs that have been translated by the C parser.
Graph refine is a collection of tools and Isabelle/HOL theories used to reason about programs in a particular graph representation.
WCET Tools are a set of tools to compute the worst-case execution time for ARM binaries.
The seL4 kernel
Channel Matrix Tools
A set of tools for generating and analysing large, sparse channel matrices.
A DSL compiler for co-generation of bitfield code and associated correctness proofs.
CAmkES is a component platform for seL4.