Reads a state transition system and performs property checking
-
Updated
Nov 5, 2024 - C++
Reads a state transition system and performs property checking
A model checker for infinite-state systems.
symbolic reachability checker
A high-performance implementation of the IC3/PDR algorithm in Rust.
An Algorithm for Checking Large Design Spaces
A reference implementation of PDR for boolean transition systems
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.
This repository acts as a centralized archive, documenting all my earned certifications relevant to Data Engineering, organized as PDF files.
Using PEGJS grammar to build a JSMF metamodel and generic model-injector coming from Google Protobuf.
Simple implementation of PDR and CAR model checking algorithms
Add a description, image, and links to the ic3 topic page so that developers can more easily learn about it.
To associate your repository with the ic3 topic, visit your repo's landing page and select "manage topics."