mCRL2org / mCRL2Links
The Git repository for the mCRL2 toolset.
☆103Updated this week
Alternatives and similar repositories for mCRL2
Users that are interested in mCRL2 are comparing it to the libraries listed below
Sorting:
- The opensmt solver☆91Updated 3 weeks ago
- The LTSmin model checking toolset☆61Updated last year
- The VerCors verification toolset for verifying parallel and concurrent software☆86Updated this week
- Definition of the Viper intermediate verification language.☆93Updated last week
- ☆61Updated 2 months ago
- Multi-engine SMT-based automatic model checker for safety properties of Lustre programs☆116Updated this week
- SRI Yices SMT Solver☆445Updated 5 months ago
- A work-in-progress language and compiler for verified low-level programming☆323Updated last week
- A Verified Compiler for Gallina, Written in Gallina☆158Updated last week
- Lem semantic definition language☆150Updated 10 months ago
- MonoSAT - An SMT solver for Monotonic Theories☆116Updated 10 months ago
- Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]☆127Updated 11 months ago
- A Library for Representing Recursive and Impure Programs in Coq☆242Updated 2 weeks ago
- SRI Sally: A model checker for infinite-state systems.☆76Updated 6 months ago
- The Eldarica model checker☆100Updated last week
- microsat☆141Updated 3 years ago
- An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logt…☆152Updated last year
- Hanoi Omega-Automata Format☆15Updated 3 years ago
- Verification-condition-generation-based verifier for the Viper intermediate verification language.☆34Updated last week
- ☆164Updated 2 weeks ago
- SAT Solver SATCH☆120Updated 3 years ago
- Tools from Pugh et al.'s "Omega Project" for constraint-based compiler tools: The "Omega Library" for constraint manipulation; The "Omega…☆72Updated 4 years ago
- Communication between Coq and SAT/SMT solvers☆163Updated this week
- Symbolic-execution-based verifier for the Viper intermediate verification language.☆127Updated last week
- Libraries useful for Dafny programs☆48Updated 5 months ago
- RISC-V Specification in Coq☆116Updated last month
- CAQE is a solver for quantified Boolean formulas☆36Updated 2 years ago
- CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory☆237Updated 2 months ago
- The DRAT-trim proof checker☆68Updated last year
- Frama-C and WP tutorial☆69Updated last month