A stream-based runtime-verification framework 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)

Runtime assertion checking based on Gospel specifications

Analysis tool for Solidity smart contracts. Prototype.

ROSMonitoring: a Runtime Verification Framework for ROS

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

Toolbox for software dependability engineering of artificial neural networks

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

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 framework for runtime monitoring.

Convert LTL formulas into finite-state automata for monitoring

A Tool for Timed Patten Matching with Automata-Based Acceleration