Formal Methods

A online playground for formal methods tools. It is a web application that allows users to run formal methods tools in the browser.

MLDiff provides a novel approach to comparing learned classifiers by translating them into SMT formulas and systematically analyzing their decision boundaries.

A Visual Studio Code extension for the SMT Z3 theorem prover. The extension provides a user-friendly interface to run the Z3 solver in the VS Code editor without installing Z3 separately.

A language server for the SMT-LIB language, providing features like syntax highlighting, autocompletion, and error checking for SMT-LIB files in various editors. It is based on Langium workbench and integrates with the Z3 SMT solver.

A language server for the Alloy specification language, providing features like syntax highlighting, autocompletion, and error checking for Alloy files in various editors. It is based on Langium workbench and integrates with the Alloy Analyzer.

A Visual Studio Code extension for the Limboole Boolean Satisfiability Solver. It supports syntax highlighting and language server features for Limboole files.