Silas: a fast, memory-efficient, explainable and verifiable ensemble trees machine learning tool. Download the education version for free now! Technical Slides, Journal Paper bibtex
Feature importance and adversarial analysis for ensemble trees/random forest machine learning models. Download for Silas Preprint bibtex
OptExplain & ProClass: global logical explanation of large ensemble trees/random forest machine learning models. Download for Silas Download for Scikit-learn Preprint bibtex
N-PAT: an extension of the model checker Process Analysis Toolkit (PAT) that allows defining (probablistic) nested models (models that use sub-models' verification results as parameters) and verifying nested models by recursive calls to PAT. Download Paper bibtex
An Isabelle/HOL formal model of SPARC TSO memory model for concurrent machine code execution. Download Paper bibtex
An executable Isabelle/HOL formal model of the VHDL language. Download Documentation
An executable Isabelle/HOL formal model of the SPARCv8 ISA and a proof of information-flow security for the LEON3 processor. Download Paper bibtex
Isabelle/HOL proof tactics for separation algebra and its extensions. Download Paper bibtex AFP Entry
A theorem prover for the assertion language of separation logic with linked lists and binary trees, based on a labelled sequent calculus and semantics compliant with symbolic heaps (A.K.A. Separata+). Download Paper bibtex
A theorem prover for the assertion language of separation logic with linked list and binary trees, based on a labelled sequent calculus and Reynolds's semantics (a variant of Separata+). Download Paper bibtex
A modular theorem prover for propositional abstract separation logics based on labelled sequent calculus (A.K.A. Separata). Download Paper bibtex
A theorem prover for BBI based on free variable labelled sequent calculus using (incomplete) heuristics. Download Paper bibtex