|
Index
| | Différents liens sur le Model-Checking
Pages Personnelles
|
Alur, Rajeev (pubs) |
|
|
|
|
Biere,
Armin |
|
|
|
|
Clarke,
Edmund M. |
Courcoubetis,
Costas (pubs) |
|
|
|
Dams,
Dennis (pubs) |
Diekert,
Volker (pubs) |
Dill, David L. |
Dwyer, Matthew (pubs) |
|
Emerson,
E. Allen |
Esparza,
Javier (pubs) |
|
|
|
Gastin,
Paul (pubs) |
Godefroid,
Patrice |
Gopalakrishnan,
Ganesh C. (pubs) |
Grumberg,
Orna (pubs) |
|
Holzmann,
Gerard |
Hulgard, Henrik (pubs) |
|
|
|
Jonsson, Bengt (pubs) |
|
|
|
|
Kick, Alexander |
Kupferman,
Orna (pubs) |
Kwiatkowska,
Marta (pubs) |
|
|
Larsen, Kim |
Lenzkes,
Dirk (pubs) |
Laroussinie, François
(pubs) |
Lee, Insup (pubs) |
|
Maler,
Oded (pubs) |
Mitchell,
John C. (pubs) |
|
|
|
Peled, Doron |
Petterson, Paul |
Pnueli,
Amir |
|
|
Ramakrishna, Y.
S. (pubs) |
Raskin,
Jean-Francois |
Ruf, Jürgen |
Rushby,
John |
|
Schlingloff,
Bernd-Holger (pubs) |
Schneider,
Klaus |
Schobbens,
Pierre-Yves |
Sistla, A.
Prasad (pubs) |
| |
Staunstrup, Jørgen
(pubs) |
|
|
|
|
Valmari, Antti |
Vardi, Moshe (pubs) |
|
|
|
Weise,
Carsten (pubs) |
Wolper,
Pierre (pubs) |
|
|
|
Yovine,
Sergio |
Yi, Wang (pubs) |
|
|
|
Zampuniéris,
Denis (pubs) |
|
|
|
Outils universitaire
| SMV |
Symbolic Model Verifier (CTL) |
| BMC |
Bounded Model Checker |
| HyTech |
The HYbrid TECHnology Tool (Automates hybrides) |
| SPIN |
Simple Promela INterpreter (LTL) |
| Kronos |
Model chekcing temps réel (TCTL) |
| MONA |
MONAdic second-order logic |
| Murphi |
|
| PEP |
Programming Environment based on Petri nets |
| PROD |
Pr/T-net reachability analysis tool (CTL + LTL) |
| RAVEN |
Real-time Analyzing and Verification ENvironment |
| TREAT |
Timed REachability Analysis Tool |
| TVS |
Transformation Verification Simulation |
| STeP |
Stanford Temporal Prover |
| SMC |
Symmetry based Model Checker (LTL) |
| UPPAAL |
Real-Time Model Checker |
| Verus |
specification and verification of real-time and other time
critical systems |
| vis |
Verification Interacting with Synthesis |
| FC2Tools |
process algebra theory |
| KIT |
Model-Checking Kit |
| Verisoft |
Lucent Technologies |
Outils commerciaux
Groupe de recherche
- Bell Labs, Murray Hill, USA, Formal
Methods at Bell Laboratories
- B User Group, BUG
- Formal Methods Europe, FME
- Basic Research in Computer Science, danemark,BRICS
- Carnegie Mellon University, USA, Model
Checking Group
- GMD, Germany, SYNCHRONIE,
Workbench for the design of synchronous systems
- GMD, Germany, VAN,
Verification and Analysis
- Helsinki University, Finland, Modelling
of Concurrency Group
- Stanford University, USA, Hardware
Verification Group
- Tampere University of Technology, Finland, Verification
Algorithm Research Group
- University of Karlsruhe, Germany, Hardware
Verification Group
Mailing lists
Liens divers
- Virtual library : formal
methods (Tous les liens sur les méthodes formelles)
- Virtual library : B
method (Tous les liens sur la methode B)
Cette page a été mise à jour le
20/08/09. |
