creators_name: Bendisposto, Jens
creators_name: Leuschel, Michael
creators_id: bendisposto@cs.uni-duesseldorf.de
creators_id: leuschel@cs.uni-duesseldorf.de
type: rodin_archive
datestamp: 2009-09-21 15:42:14
lastmod: 2010-04-19 15:05:57
metadata_visibility: show
title: Proof Assisted Model Checking for B
subjects: deploy_tooldev_modela
subjects: Event-Bsemantics
subjects: deploy_method_proof
full_text_status: public
abstract: 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) pomc_paper.zip: Contains the model that is guaranteed to terminate, but assumes finite(STATES)

2) pomc paper-wo_termination.zip: Contains the model without the assumption, but does not guarantee termination
citation:   Bendisposto, Jens and Leuschel, Michael   Proof Assisted Model Checking for B.  [Rodin Archive]     
document_url: http://deploy-eprints.ecs.soton.ac.uk/152/2/pomc_paper-wo_termination.zip
document_url: http://deploy-eprints.ecs.soton.ac.uk/152/3/pomc_paper.zip