《Hello 算法》：动画图解、一键运行的数据结构与算法教程。支持简中、繁中、English、日本語，提供 Python, Java, C++, C, C#, JS, Go, Swift, Rust, Ruby, Kotlin, TS, Dart 等代码实现

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

An easy-to-learn/use static analysis framework for Java

Tai-e assignments for static program analysis

The Ultimate program analysis framework.

Runtime verification system for Java, using AspectJ for instrumentation.

An event stream processor anyone can use

RV-Monitor core system code

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

Prototype of "Automata-Guided Control-Flow-Sensitive Fuzz Driver Generation". Forked for potential update.

Larva is a runtime verification tool which compiles enriched state machine specifications into runtime monitors which connect with Java systems through AspectJ.

Fuzz drivers are essential for fuzzing library APIs. However, manually composing fuzz drivers is difficult and time consuming. That's why we propose Rubick, which is an automata-based fuzz driver g…

Automated Sound Security Analysis of Smart Contracts

Various utilities for working with the Etherem Reference Tests.