TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

The Ultimate program analysis framework.

A free, open-source Java library for automata, graphs, and transition systems

Static checker for Java

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms

DARPA's Cyber Assured Systems Engineering (CASE) project named Verification Evidence and Resilient Design in Anticipation of Cybersecurity Threats (VERDICT)

ModelPolisher accesses the BiGG Models knowledgebase to annotate SBML models.

Command line tool for model checking using LTL, CTL and CTL* formulas

A Class Field Value Validation Library.

A Shape Analysis Tool based on Graph Grammars

A compiler developed using ANTLR in Java that translates Solidity smart contracts into mCRL2 models

Formal verification engine for Verilog with built-in support for simulating flip-flop metastability

A Java library that allows you to check whether a given transition system (described as a Kripke structure) satisfies a given computation tree logic (CTL) formula.

A test generator application designed to create performance benchmarks for SymploeoPC

Property Specification Patterns for UPPAAL

This repository is a source code of my master thesis. In my master thesis, I developed a prototype to translate TLA+ expressions to the SMT-LIB language, and to verify safety properties with SMT solvers, IC3-based techniques and user-guided predicate abstraction.

A Java framework for the creation and simulation of bigraphs.

Converter of function block models from NuSMV to Promela (SPIN)

This project's objective is to program a model checking software that verifies the validity of a CTL formula on the initial state of a finite automaton.

Validates the integrity of a furniture by checking it's parts