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

The Ultimate program analysis framework.

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 compiler developed using ANTLR in Java that translates Solidity smart contracts into mCRL2 models

A Shape Analysis Tool based on Graph Grammars

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.

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

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.

A generic bounded model checker.

A Java framework for the creation and simulation of bigraphs.

Experimental system model generator for RTS