Cardio aims to be a probabilistic model checking engine for deterministic Markov chains, i.e., CTMCs and DTMCs, written in Rust and eventually verified using Kani and/or Verus. Using Rust best-practice, Cardio wishes to be:
- modular
- efficient
- fast
- customizable
We would like Cardio to be competitive in speed to Storm.
- CSL and PCTL parsing (in progress--mostly finished)
- Rewards
- Transient analysis (in progress)
- Steady State Analysis (planned)
...and more.
Cardio is licensed under the GNU General Public License v3. It is open source software, free as in free speech, and always will be.
Cardio is developed at Utah State University in Logan, UT, USA.