Software
From time to time we release software as open source, or occasionally under a binary-only licence.
Github
You can find most of our software on github:
- http://github.com/au-ts: Our main repository
- http://github.com/sel4: The repository of the seL4 Foundation, some of our projects migrate there after being adopted by the Foundation
- http://github.com/sel4proj: This is an unmaintained repo of seL4-related work that generally proceeds the seL4 Foundation.
Specific projects with their own repos
CakeML
CakeML is an impure functional language with an end-to-end-verified optimizing compiler. The code can be found at https://code.cakeml.org/.
Former Projects
Unmaintained repos of some of our former projects.
Cogent
Cogent is a programming language with a certifying compiler for developing high-assurance systems components. The code can be found at https://github.com/NICTA/cogent/.
AutoCorres
AutoCorres is an Isabelle/HOL tool that automatically abstracts and simplifies programs that have been translated by the C parser.
Graph refine
Graph refine is a collection of tools and Isabelle/HOL theories used to reason about programs in a particular graph representation.
WCET tools
WCET Tools are a set of tools to compute the worst-case execution time for ARM binaries.
Channel Matrix Tools
A set of tools for generating and analysing large, sparse channel matrices.
Bitfield Generator
A DSL compiler for co-generation of bitfield code and associated correctness proofs.
CAmkES
CAmkES is a component platform for seL4.
eCrhonos
eChronos is an RTOS for MMU-less microcontrollers.