Projects
For legacy projects, please visit my GitHub profile.
MLDiff
MLDiff provides a novel approach to comparing learned classifiers by translating them into SMT formulas and systematically analyzing their decision boundaries.
FM Playground
A online playground for formal methods tools. It is a web application that allows users to run formal methods tools in the browser.
Alloy LSP
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.
SMT-LIB LSP
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.
VS Code Extension for SMT-LIB (Z3)
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.
VS Code Extension for Limboole
A Visual Studio Code extension for the Limboole Boolean Satisfiability Solver. It supports syntax highlighting and language server features for Limboole files.