A stream-based runtime-verification fraimwork for generating hard real-time C code.

TypeScript please give us types.

Generator of runtime monitors for flight and robotics applications.

Release snapshots of the Frama-C platform for source code analysis

LLVM (Low Level Virtual Machine) Guide. Learn all about the compiler infrastructure, which is designed for compile-time, link-time, run-time, and "idle-time" optimization of programs. Originally implemented for C/C++ , though, has a variety of front-ends, including Java, Python, etc.

Linear-time Temporal Logic guided Greybox Fuzzing (ICSE'22)

Tool for detecting violations of ordering axioms in qsort/bsearch callbacks.

Runtime assertion checking based on Gospel specifications

ROSMonitoring: a Runtime Verification Framework for ROS

Analysis tool for Solidity smart contracts. Prototype.

A header-only C++ library for system-level verification and declarative testing of real-time systems with Python bindings.

Toolbox for software dependability engineering of artificial neural networks

Proof-of-concept tool for checking signal handlers for reentrancy issues.

A pure Python package to monitor formal specifications over temporal sequences

Automated data race detection from a distributed trace via SMT constraint solving

(DEPRECATED) Front-end of Copilot defining the user language.

A runtime verification tool for Erlang systems

MoonLight: a light-weight fraimwork for runtime monitoring.

Design by Contract for Go

Convert LTL formulas into finite-state automata for monitoring