| Andromeda |
Andromeda 2 is a proof checker for user-definable dependently-typed theories.
|
| Gillian |
Gillian is a multi-language analysis platform supporting, e.g., verification and symbolic testing. … |
| Holbert |
Holbert is an interactive theorem prover, or proof assistant, based on higher order logic and … |
| ivory-rtverification |
[ Not Maintained Since 2014 ] Runtime verification for C code via a GCC plugin architecture.
|
| RbSyn |
Program synthesis for Ruby
|
| cvc4 |
[ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … |
| cvc5 |
cvc5 is an automatic theorem prover for SMT problems.
|
| ESBMC |
ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying … |
| Intrepyd |
[ Not Maintained Since 2021 ] Intrepyd is a python module that provides a simulator and a model … |
| LTSmin |
LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the … |
| Vampire |
Vampire is a theorem prover.
|