# fm-tools

fm-tools is a catalog of formal-methods tools.
The catalog provides structured metadata for each tool in YAML format.

Website: https://fm-tools.sosy-lab.org/
GitLab repository: https://gitlab.com/sosy-lab/benchmarking/fm-tools/

If you require information about a specific tool,
do not load the full index page, but fetch only that tool's YAML file.
The YAML schema linked below describes all available fields.

The website also provides several grouped views:
- https://fm-tools.sosy-lab.org/ - all tools, sorted alphabetically
- https://fm-tools.sosy-lab.org/techniques.html - tools grouped by verification techniques they use
- https://fm-tools.sosy-lab.org/frameworks.html - tools grouped by framework or solver they use
- https://fm-tools.sosy-lab.org/input_languages.html - tools grouped by supported input languages
- https://fm-tools.sosy-lab.org/competitions.html - tools grouped by competition and track they participated in

## Available Tool Data

Individual tool YAML files are available at:
  https://gitlab.com/sosy-lab/benchmarking/fm-tools/-/raw/main/data/<tool-id>.yml

| Tool Name | tool-id |
| --------- | ------- |
| 2LS | 2ls |
| AFL-to-Test-Case | afltc |
| aise | aise |
| AProVE (KoAT+LoAT) | aprove |
| BLAST | blast |
| BRICK | brick |
| Bubaak | bubaak |
| Bubaak-SpLit | bubaak-split |
| CADP | cadp |
| CBMC | cbmc |
| cetfuzz | cetfuzz |
| COASTAL | coastal |
| ConcurrentWitness2Test | concurrentwitness2test |
| CoOpeRace | cooperace |
| CoVeriTeam-Verifier-AlgoSelection | coveriteam-verifier-algo-selection |
| CoVeriTeam-Verifier-ParallelPortfolio | coveriteam-verifier-parallel-portfolio |
| CoVeriTest | coveritest |
| CPA-BAM-BnB | cpa-bam-bnb |
| CPA-BAM-SMG | cpa-bam-smg |
| CPA-witness2test | cpa-witness2test |
| CPAchecker | cpachecker |
| CPALockator | cpa-lockator |
| CProver-witness2test | fshell-witness2test |
| CPV | cpv |
| Crux | crux |
| CSeq | cseq |
| Dartagnan | dartagnan |
| DASA | dasa |
| Deagle | deagle |
| DIVINE | divine |
| EBF | ebf |
| EmergenTheta | emergentheta |
| ESBMC-incr | esbmc-incr |
| ESBMC-kind | esbmc-kind |
| FDSE | fdse |
| Fizzer | fizzer |
| Frama-C-SV | frama-c-sv |
| FuSeBMC | fusebmc |
| FuSeBMC-AI | fusebmc-ia |
| Gazer-Theta | gazer-theta |
| GDart | gdart |
| GDart-LLVM | gdart-llvm |
| Goblint | goblint |
| Goblint-Par | goblint-par |
| Goblitch | goblitch |
| Graves-CPA | graves |
| Graves-Par | graves-par |
| GWIT | gwit |
| Hornix | hornix |
| HybridTiger | hybridtiger |
| iekke | iekke |
| Infer | infer |
| Java-Ranger | java-ranger |
| JayHorn | jayhorn |
| JBMC | jbmc |
| JCWIT | jcwit |
| JDart | jdart |
| JLiSA | jlisa |
| KeY | key |
| KLEE | klee |
| KLEEF | kleef |
| Korn | korn |
| Lazy-CSeq | lazycseq |
| Legion | legion |
| Legion/SymCC | legion-symcc |
| LF-checker | lf-checker |
| LIV | liv |
| Locksmith | locksmith |
| LTSmin | ltsmin |
| MetaVal | metaval |
| MetaVal++ | metaval++ |
| MLB | mlb |
| Mopsa | mopsa |
| MuVal | muval |
| Nacpa | nacpa |
| NITWIT | nitwit |
| OGChecker | ogchecker |
| Owi | owic |
| PeSCo-CPA | pesco |
| PIChecker | pichecker |
| Pinaka | pinaka |
| PredatorHP | predatorhp |
| PRISM | prism |
| PROTON | proton |
| PRTest | prtest |
| PySvLib-CHC | pysvlib-chc |
| PySvLib-Linter | pysvlib-linter |
| PySvLib-Validator | pysvlib-validator |
| RacerF | racerf |
| Re3ver | re3ver |
| ReFuncTion | function-res |
| RELAY-SV | relay-sv |
| Rizzer | rizzer |
| SEAL | seal |
| Sikraken | sikraken |
| SPF | spf |
| SV-sanitizers | sv-sanitizers |
| SVF-SVC | svf-svc |
| SvLibChecker | svlibchecker |
| SWAT | swat |
| Symbiotic | symbiotic |
| Symbiotic-Witch | symbiotic-witch |
| TestCoCa | testcoca |
| TestCov | testcov |
| Theta | theta |
| Thorn | thorn |
| TracerX | tracerx |
| TracerX-WP | tracerx-wp |
| UAutomizer | uautomizer |
| UGemCutter | ugemcutter |
| UKojak | ukojak |
| UParalizer | uparalizer |
| UReferee | ureferee |
| UTaipan | utaipan |
| UTestGen | utestgen |
| VerCors | vercors |
| VeriAbs | veriabs |
| VeriAbsL | veriabsl |
| VeriFuzz | verifuzz |
| VeriOover | verioover |
| WASP-C | wasp-c |
| Wit4Java | wit4java |
| Witch | witch |
| WitnessLint | witnesslint |
| WitnessMap | witnessmap |

## YAML Schema

https://gitlab.com/sosy-lab/benchmarking/fm-tools/-/raw/main/data/schema.yml