Benchmarks for Symbolic Model Checking

This repository contains benchmark model-checking models with associated temporal logic formulas. Real-life, full-scale model-checking instances and design spaces are often hard to find in published literature; we collect them here.

There are also language translators that translate one high-level modeling language to another so that, e.g., Verilog models can be translated into SMV. This enables experiments validating and profiling language translators as well as growing the collection of model-checking benchmarks.