Model Checker
Eine nicht vollständige Liste von Model Checkern.
Klassische Model Checker
Model Checker für zustandsendliche Systeme.
Explizite Model Checker
- SPIN von Gerard J. Holzmann, Bell
Labs/jetzt NASA JPL, mit den Erweiterungen
- dSPIN für
höhere Programmiersprachen, Verimag
- DT-SPIN,
Erweiterung um "discrete time", TU Eindhoven
- HSF-SPIN, Erweiterung um heuristische Suche, Uni Freiburg
- LWAASpin,
Erweiterung um lineare schwache alternierende Automaten, Uni München
- PSPIN,
Erweiterung für distributed memory, Uni Turin
- RT-SPIN,
Erweiterung um real time, Verimag
- jSpin, eine alternative Oberfläche für SPIN, Weizmann Institute of Science
- Murphi, Stanford University
- TLC,
ein Model Checker für TLA
- VeriSoft,
Bell Labs, ein Software Model Checker
Symbolische Model Checker
- SMV, CMU
- Cadence-SMV,
Kenneth McMillan, Cadence Labs
- NuSMV, ITC-IRST, Università degli Studi di Genova
- SMI, Verimag
- Mucke, Uni Karlsruhe
- MOCHA,
Berkely, University of Pennsylvania, Stony Brook
- VIS, Berkeley
Bounded Model Checker
- BMC, ETH Zürich
- NuSMV, ITC-IRST, Università degli Studi di Genova
- mu-Sabre, Uni München
Model Checking Suites
- AVISPA Project, DIST Genova, INRIA Nancy, ETH Zürich, Siemens AG
- SAL, Stanford Research Institute
Model Checker für zustandsunendliche Systeme
Sourcecode Model Checker
- Moped, Uni Stuttgart
- BLAST, Berkeley
- MAGIC, CMU
- SLAM, Microsoft Research,
mit Erweiterungen:
- SATabs, CMU
- Zing, Microsoft Research
- Bogor, Teil des Bandera projects, SAnToS Laboratory
- JavaPathFinder, NASA
- MOPS, Berkeley
- CBMC, CMU
Realtime Model Checker
Model Checker für hybride Automaten
Probabilistische Model Checker
Andere
Ergänzungen und Korrekturen bitte an hammer "at" pst . ifi . lmu . de senden!