Industrial deployment of system engineering methods providing high dependability and productivity


Proof Assisted Model Checking for B

Bendisposto, Jens and Leuschel, Michael Proof Assisted Model Checking for B. [Rodin Archive]

[img]ZIP Archive (Proof Supported Model Checking (w/o termination))
[img]ZIP Archive (Proof Supported Model Checking)


The archives contain the models for proof supported model checking. For detailed description see Bendisposto, Leuschel: Proof Assisted Model Checking for B Proceedings of International Conference on Formal Engineering Methods (ICFEM 09), LNCS, to appear 1) Contains the model that is guaranteed to terminate, but assumes finite(STATES) 2) pomc Contains the model without the assumption, but does not guarantee termination

Item Type:Rodin Archive
Subjects:Tool developments > Model checking
Methodology > Proof and model checking
ID Code:152
Deposited By:Jens Bendisposto
Deposited On:21 Sep 2009 16:42
Last Modified:19 Apr 2010 16:05

Repository Staff Only: item control page

Deploy-Project - All right reserved